Abdellah EL Mekki, Samar M. Magdy, Houdaifa Atou, Ruwa AbuHweidi, Baraah Qawasmeh, Omer Nacar, Thikra Al-hibiri, Razan Saadie, Hamzah A. Alsayadi, Nadia Ghezaiel Hammouda, Alshima Mohammed Alkhazimi, Aya Hamod, Al-Yas Yaqoob Al-Ghafri, Wesam El-Sayed, Asila Ismail al Sharji, Mohamad Ballout, Anas Belfathi, Karim Ghaddar, Serry Sibaee, Alaa Aoun, Aeej Mohammed Aseri, Lina Abureesh, Ahlam Bashiti, Majdal Yousef, Abdulaziz Hafiz, Yehdih Mohamed, Emira Hamedtou, Brakehe Emehah, Rahaf Alhamouri, Youssef Nafea, Aya El Aatar, Walid Al-Dhabyani, Emhemed S. Hamed, Sara Shatnawi, Fakhraddin Alwajih, Khalid Elkhidir, Ashwag Alasmari, Abdurrahman Gerrio, Omar Said Alshahri, AbdelRahim A. Elmadany, Ismail Berrada, Amir Azad Adli Al-kathiri, Fadi Zaraket, Mustafa Jarrar, Yahya Mohamed EL Hadj, Hassan Alhuzali, Muhammad Abdul-Mageed. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2026.

This paper presents R-BPE, a lightweight framework for adapting existing Byte-Pair Encoding (BPE) tokenizers to better support a specified target language.It reuses tokens from user-excluded languages and creates ID-based maps to resolve the new tokens of the chosen language.We evaluate R-BPE on Arabic as a target language.R-BPE reduced subword fertility by an average of 24.4% across the LLaMA 3.1 8B, Command R 35B, and Qwen 3 8B models.Applied to LLaMA 3.1 8B in continued pretraining mode, R-BPE yields a 7.33% reduction in training time.On the ArabicMMLU benchmark, the resulting model improved by 5.09 points on five in-domain topics and matched the original model's overall performance.It also preserved performance on EnglishMMLU.R-BPE effectively leverages existing models' tokenizers, embedding layers, and performance to better support target languages without incurring model size changes.We release an R-BPE implementation that is compatible with HuggingFace interfaces and thereby readily applicable to a wide range of existing models at https://acr.ps/1L9GPmL.

This article presents morphologically-annotated Yemeni, Sudanese, Iraqi, and Libyan Arabic dialects (${\text{L}\hat{\text{i}}\text{sa}\bar{\text{n}}}$) corpora. ${\text{L}\hat{\text{i}}\text{sa}\bar{\text{n}}}$ features around 1.2 million tokens. We collected the content of the corpora from several social media platforms. The Yemeni corpus ($\tilde 1.05{\text{M}}$ tokens) was collected automatically from Twitter. The corpora of the other three dialects ($\tilde 50{\text{K}}$ tokens each) was manually collected from Facebook and YouTube posts and comments. Thirty-five (35) annotators who are native speakers of the target dialects carried out the annotations. The annotators segmented all words in the four corpora into prefixes, stems and suffixes and labeled each with different morphological features such as part of speech, lemma, and a gloss in English. We developed the Arabic Dialect Annotation Toolkit (ADAT) to assist the annotators and to ensure compatibility with SAMA and Curras tagsets. We trained annotators on a set of guidelines and on how to use ADAT. ADAT is open source, and the four corpora are available at https://sina.birzeit.edu/currasat.

This paper presents two-fold contributions: a full revision of the Palestinian morphologically annotated corpus (Curras), and a newly annotated Lebanese corpus (Baladi). Both corpora can be used as a more general Levantine corpus. Baladi consists of around 9.6K morphologically annotated tokens. Each token was manually annotated with several morphological features and using LDC’s SAMA lemmas and tags. The inter-annotator evaluation on most features illustrates 78.5% Kappa and 90.1% F1-Score. Curras was revised by refining all annotations for accuracy, normalization and unification of POS tags, and linking with SAMA lemmas. This revision was also important to ensure that both corpora are compatible and can help to bridge the nuanced linguistic gaps that exist between the two highly mutually intelligible dialects. Both corpora are publicly available through a web portal.

Words in Arabic consist of letters and short vowel symbols called diacritics inscribed atop regular letters. Changing diacritics may change the syntax and semantics of a word; turning it into another. This results in difficulties when comparing words based solely on string matching. Typically, Arabic NLP applications resort to morphological analysis to battle ambiguity originating from this and other challenges. In this article, we introduce three alternative algorithms to compare two words with possibly different diacritics. We propose the Subsume knowledge-based algorithm, the Imply rule-based algorithm, and the Alike machine-learning-based algorithm. We evaluated the soundness, completeness, and accuracy of the algorithms against a large dataset of 86,886 word pairs. Our evaluation shows that the accuracy of Subsume (100%), Imply (99.32%), and Alike (99.53%). Although accurate, Subsume was able to judge only 75% of the data. Both Subsume and Imply are sound, while Alike is not. We demonstrate the utility of the algorithms using a real-life use case -- in lemma disambiguation and in linking hundreds of Arabic dictionaries.

Design-for-test, logic built-in self-test, memory technology mapping, and clocking concerns require team-months of verification time as they traditionally happen at gate-level. We present a novel concern-oriented methodology that enables automatic insertion of these concerns at the register-transfer-level where verification is easier. The methodology involves three main phases: 1) flipflop inference and instantiation algorithms that handle parametric register transfer level (RTL) modules; 2) transformations that take entry RTL and produce RTL modules where memory elements are separated from functionality; and 3) a concern weaving tool that automatically inserts memory related design concerns implemented in recipe files into the RTL modules. The transformation is sound as proven and validated by equivalence checking using formal verification. We implemented the methodology in a tool that is currently used in an industrial setting wherein it reduced design verification time by more than 40%. The methodology is also effective with open source embedded system frameworks.

We present a criterion for checking local and global deadlock freedom of finite state systems expressed in BIP: a component-based framework for constructing complex distributed systems. Our criterion is evaluated by model-checking a set of subsystems of the overall large system. If satisfied in small subsystems, it implies deadlock-freedom of the overall system. If not satisfied, then we re-evaluate over larger subsystems, which improves the accuracy of the check. When the subsystem being checked becomes the entire system, our criterion becomes complete for deadlock-freedom. Hence our criterion only fails to decide deadlock freedom because of computational limitations: state-space explosion sets in when the subsystems become too large. Our method thus combines the possibility of fast response together with theoretical completeness. Other criteria for deadlock freedom, in contrast, are incomplete in principle, and so may fail to decide deadlock freedom even if unlimited computational resources are available. Also, our criterion certifies freedom from local deadlock, in which a subsystem is deadlocked while the rest of the system executes. Other criteria only certify freedom from global deadlock. We present experimental results for dining philosophers and for a multi-token-based resource allocation system, which subsumes several data arbiters and schedulers, including Milner’s token-based scheduler.

Summary Oracles used for testing graphical user interface (GUI) programmes are required to take into consideration complicating factors such as variations in screen resolution or colour scheme when comparing observed GUI elements with expected GUI elements. Researchers proposed fuzzy comparison rules and computationally expensive image processing techniques to tame the comparison process because otherwise the naïve matching comparison would be too constraining and consequently impractical. Alternatively, this paper proposes GUICop, a novel approach with a supporting toolset that takes (1) a GUI programme and (2) user‐defined GUI specifications characterizing the rendering behaviour of the GUI elements and checks whether the execution traces of the programme satisfy the specifications. GUICop comprises the following: (1) a GUI Specification Language; (2) a Driver; (3) Instrumented GUI Libraries; 4) a Solver; and (5) a Code Weaver. The user defines the specifications of the subject GUI programme using the GUI Specification Language. The Driver traverses the GUI structure of the programme and generates events that drive its execution. The Instrumented GUI Libraries capture the GUI execution trace, ie, information about the positions and visibility of the GUI elements. And the Solver, enabled by code injected by the Code Weaver, checks whether the traces satisfy the specifications. GUICop was successfully evaluated using 4 open source GUI applications that included 8 defects, namely, Jajuk, Gason, JEdit, and TerpPaint.

Summary The goal of regression testing is to ensure that the behaviour of existing code, believed correct by previous testing, is not altered by new program changes. This paper argues that the primary focus of regression testing should be on code associated with (1) earlier bug fixes and (2) particular application scenarios considered to be important by the developer or tester. Existing coverage criteria do not enable such focus, for example, 100% branch coverage does not guarantee that a given bug fix is exercised or a given application scenario is tested. Therefore, there is a need for a new and complementary coverage criterion in whichthe user can defineatest requirement characterizing a given behaviour to be coveredas opposed to choosing from a pool of pre‐defined and generic program elements. This paper proposes this new methodology and calls itUCov, auser‐defined coverage criterionwherein a test requirement is anexecution patternof program elements, and possibly predicates, that a test case must satisfy. The proposed criterion is not meant to replace existing criteria, but to complement them as it focuses the testing on important code patterns that could go untested otherwise.UCovsupportstest case intent verification. For example, following a bug fix, the testing team may augment the regression suite with the test case that revealed the bug. However, this test case might become obsolete due to code modifications not related to the bug. But if a test requirement characterizing the bug was defined by the user,UCovwould determine that test case intent verification failed. TheUCovmethodology was implemented for the Java platform, was successfully applied onto 10 real‐life case studies and was shown to have advantages overJUnit. The implementation comprises the following tools: (1)TRSpec: allows the user to easily specify complex test requirements; (2)TRCheck: checks whether user‐defined test requirements were satisfied, that is, supports test case intent verification; and (3)TRMigrate: migrates user‐defined test requirements to subsequent versions of a given program. Copyright © 2016 John Wiley & Sons, Ltd.

Static verification techniques leverage Boolean formula satisfiability solvers such as SAT and SMT solvers that operate on conjunctive normal form and first order logic formulae, respectively, to validate programs. They force bounds on variable ranges and execution time and translate the program and its specifications into a Boolean formula. They are limited to programs of relatively low complexity for the following reasons. (1) A small increase in the bounds can cause a large increase in the size of the translated formula. (2) Boolean satisfiability solvers are restricted to using optimizations that apply at the level of the formula. Finally, (3) the Boolean formulae often need to be regenerated with higher bounds to ensure the correctness of the translation. We present a method that uses And-Inverter-Graph (AIG) sequential circuits, and AIG synthesis and verification frameworks to validate programs. An AIG is a Boolean formula with memory elements, logically complete negated conjunction gates, and a hierarchical structure. Encoding the validation problem of a program as an AIG (1) typically provides a more succinct representation than a Boolean formulae encoding with no memory elements, (2) preserves the high-level structure of the program, and (3) enables the use of a number of powerful automated analysis techniques that have no counterparts for other Boolean formulae such as CNF. Our method takes an imperative program with a first order logic specification consisting of a precondition and a postcondition pair, and a bound on the program variable ranges, and produces an AIG with a designated output that is${true}$when the program violates the specification. Our method uses AIG synthesis reduction techniques to reduce the AIG, and then uses AIG verification techniques to check the satisfiability of the designated output. The results show that our method can validate designs that are not possible with other state of the art techniques, and with bounds that are an order of magnitude larger.

Computational linguistic and natural language processing automation tasks require text annotated with tags that represent the desired output of the task. The annotation tags serve for training, validation, and evaluation. Arabic morphological analysis, and tags associated with it such as part of speech and gloss tags, is key to Arabic computational linguistics and natural language processing. Several manual and automated tagging tools exist for text. Very few exist that are based on Arabic morphological analysis. In this paper, we present an open source tagging tool with visual interface that enables the construction of annotated Arabic text corpora with automatic morphology-based tags. The tool allows the specification of tags with Boolean formulae where the atomic predicates are match and contain relations between the morphological solution of part of the text and the value of a morphological feature. The tool allows the user to directly enter manual tags, to edit existing tags through a tag sensitive coloring interface, to compare tag sets, and compute accuracy results.

The majority of dynamic software analyses are implemented in the form of fully-automated techniques. Given the limited success of many of these techniques, we explore the use of visualization as the basis for alternative techniques. Specifically, we investigate the use of multivariate visualization scatter plots, which aim at presenting high dimensional data in low dimensions (e.g., 2D). For example, to visualize the similarity between test cases, where a test is represented as a scatter point, the execution profiles induced by the test cases are compared in order to calculate similarity metrics that will characterize the distances between the scatter points. This type of scatter plots was previously presented by other researchers who also suggested their use in several software analyses. This work considers these scatter plots in: 1) identifying coincidentally correct tests which are a safety reducing factor in coverage based fault localization, and 2) outlining a user aided visualization-based fault localization technique. Other applications of multivariate visualization to software analysis will also be discussed.

Typically, oracles used to test graphical user interface(GUI) programs highly depend on environmental factors that are not related to the functionality of the program, such as screen resolution and color schemes. To accommodate these on-functional variations, researchers suggested fuzzy comparison rules that determine whether the output of a GUI program matches the oracles. Others suggested computer vision based solutions that make use of computationally expensive image processing techniques to abstract the strict comparisons. Alternatively, we propose GUICOP, a system that checks whether a trace of a GUI execution violates a given GUI specification. GUICOP is composed of a GUI specification language, instrumented GUI libraries, and a checker. The alphabet of the specification language contains basic geometric shapes describing GUI components, events, and positional and temporal operators that express relative object positions and event timings, respectively. During program execution, the instrumented libraries capture positional and temporal information of components and associated triggered events in execution traces. The checker determines whether the traces satisfy the specifications. To evaluate GUICOP, we wrote 50 use cases that describe real GUI applications and used the GUICOP checker on the supported cases that successfully revealed violations.

Embedded systems typically consist of a composition of a set of hardware and software IP modules. Each module is heavily optimized by itself. However, when these modules are composed together, significant additional opportunities for optimizations are introduced because only a subset of the entire functionality is actually used. We propose COSE-a technique to jointly optimize such designs. We use symbolic execution to compute invariants in each component of the design. We propagate these invariants as constraints to other modules using global flow analysis of the composition of the design. This captures optimizations that go beyond, and are qualitatively different than, those achievable by compiler optimization techniques such as common subexpression elimination, which are localized. We again employ static analysis techniques to perform optimizations subject to these constraints. We implemented COSE in the Metropolis platform and achieved significant optimizations using reasonable computational resources.

The alloy tool-set has been gaining popularity as an alternative to traditional manual testing and checking for design correctness. Alloy uses a first-order relational logic for modeling designs. The alloy analyzer translates alloy formulas for a given scope, i.e., a bound on the universe of discourse, to Boolean formulas in conjunctive normal form (CNF), which are subsequently checked using prepositional satisfiability solvers. We present SERA, a novel algorithm that compiles a relational logic formula for a given scope to a sequential circuit. There are two key advantages of sequential circuits: they form a more succinct representation than CNF formulas, sometimes by several orders of magnitude. Also sequential circuits are amenable to a range of powerful automatic analysis techniques that have no counterparts for CNF formulas. Our experiments show that SERA, used in conjunction with a sequential circuit analyzer, can check formulas for scopes that are an order of magnitude higher than those feasible with the alloy analyzer.

A number of researchers have proposed the use of Boolean satisfiability solvers for verifying C programs. They encode correctness checks as Boolean formulas using finitization: loops and recursion are bounded, as is the size of the input instances. The SAT approach has been shown to find subtle bugs with reasonable resources. However, it does not scale well; in particular, it lacks the ability to handle larger bounds. We present SEBAC, which can handle the same class of programs as the SAT approach, and scales to bounds that are orders of magnitude higher. The key difference between SEBAC and SAT techniques is SEBAC's use of imperative Boolean sequential circuits, which are Boolean formulas with memory elements instead of the Boolean formulas which are stateless

State-equivalence based reduction techniques, e.g. bisimulation minimization, can be used to reduce a state transition system to facilitate subsequent verification tasks. However, the complexity of computing the set of equivalent state pairs often exceeds that of performing symbolic property checking on the original system. We introduce a fully-automated efficient compositional minimization approach which requires only static analysis. Key to our approach is a heuristic algorithm that identifies components with high reduction potential in a bit-level netlist. We next inject combinational logic which restricts the component's inputs to selected representatives of symbolically-computed equivalence classes thereof. Finally, we use existing transformations to synergistically exploit the dramatic netlist reductions enabled by these input filters. Experiments confirm that our technique is able to efficiently yield substantial reductions on large industrial netlists.