| 1. |
- Abdulla, Parosh, Professor, 1961-, et al.
(author)
-
On the Separability Problem of String Constraints
- 2020
-
In: 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference). - Dagstuhl, Germany. - 9783959771603 ; , s. 16:1-16:19
-
Conference paper (peer-reviewed)abstract
- We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an ExpSpace algorithm for the separability of a useful class of straight-line string constraints, and a Pspace-hardness result.
|
|
| 2. |
- Abdulla, Parosh, Professor, 1961-, et al.
(author)
-
On the State Reachability Problem for Concurrent Programs Under Power
- 2020
-
In: Networked Systems - 8th International Conference, {NETYS} 2020, Morocco, Revised Selected Papers. - : Springer Nature Switzerland AG.
-
Conference paper (peer-reviewed)abstract
- We consider the problem of safety verification, formalized as control-state reachability, for concurrent programs running on the Power architecture. Our main result shows that safety verification under Power is undecidable for programs with just two threads.
|
|
| 3. |
- Abdulla, Parosh, Professor, 1961-, et al.
(author)
-
Optimal Stateless Model Checking for Causal Consistency
- 2023
-
In: Tools and Algorithms for the Construction and Analysis of Systems. - : Springer. - 9783031308239 - 9783031308222 ; , s. 105-125
-
Conference paper (peer-reviewed)abstract
- We present a framework for efficient stateless model checking (SMC) of concurrent programs under three prominent models of causal consistency, . Our approach is based on exploring traces under the program order and the reads from relations. Our SMC algorithm is provably optimal in the sense that it explores each and relation exactly once. We have implemented our framework in a tool called Conschecker. Experiments show that Conschecker performs well in detecting anomalies in classical distributed databases benchmarks.
|
|
| 4. |
|
|
| 5. |
- Abdulla, Parosh, Professor, 1961-, et al.
(author)
-
Verification under Intel-x86 with Persistency
- 2024
-
In: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 8:PLDI
-
Journal article (peer-reviewed)abstract
- The full semantics of the Intel-x86 architecture has been defined by Raad et al in POPL 2022, extending the earlier formalization based on the TSO memory model incorporating persistency. This new semantics involves an intricate combination of the SC, TSO, and PSO models to account for the diverse features of the enlarged instruction set. In this paper we investigate the reachability problem under this semantics, including both its consistency and persistency aspects each of which requires reasoning about unbounded operation reorderings. Our first contribution is to show that reachability under this model can be reduced to reachability under a model without the persistency component. This is achieved by showing that the persistency semantics can be simulated by a finite-state protocol running in parallel with the program. Our second contribution is to prove that reachability under the consistency model of Intel-x86 (even without crashes and persistency) is undecidable. Undecidability is obtained as soon as one thread in the program is allowed to use both TSO variables and two PSO variables. The third contribution is showing that for any fixed bound on the alternation between TSO writes (write-backs), and PSO writes (non-temporal writes), the reachability problem is decidable. This defines a complete parametrized schema for under-approximate analysis that can be used for bug finding.
|
|
| 6. |
- Bui, Phi Diep
(author)
-
On Solving String Constraints
- 2021
-
Doctoral thesis (other academic/artistic)abstract
- Software systems are deeply involved in diverse human activities as everyone uses a variety of software systems on a daily basis. It is essential to guarantee that software systems all work correctly. Two popular methods for finding failures of software systems are testing and model checking. Various efficient testing and model checking approaches are satisfiability-based, where the core of the approaches is Satisfiability Modulo Theories (SMT) solvers for solving the path feasibility and/or reachability problems. The significant growth of string manipulating programs in modern programming languages, including Python and JavaScript, demands SMT solvers being capable of analysing string constraints. This thesis proposes two frameworks for checking the satisfiability of extensive classes of string constraints, discovers a new decidable fragment of string constraints, and introduces efficient solvers for solving string constraints.The first framework for checking the satisfiability of string constraints is based on Counter-Example Guided Abstract Refinement (Cegar) procedure, and applicable to diverse classes of string constraints. It is worth mentioning that the framework is the first one ever that can support both context-free membership and transducer constraints. The framework has two components: under-approximation and over-approximation. The under-approximation uses flat automata to restrict the search for a solution to only strings generated by a flat automaton. The over-approximation abstracts the input constraints and produces a counter-example of the abstraction. In the second framework for checking the satisfiability string constraints, the under-approximation uses parametric flat automata to restrict the domain of variables, thus allows better performance. Furthermore, the second framework is capable of solving string-number conversion constraints. It is a crucial characteristic since string-number conversion is a part of the definition of core semantics in numerous program languages such as Python and JavaScript. The thesis introduces a new decidable fragment of string constraints, called weakly-chaining. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. The new decidable fragment is empirically useful as it helps string solvers guarantee termination in many more cases since the solvers do not provide any guarantee of termination to handle string constraints in general.The thesis also presents three efficient solvers for solving string constraints, called Trau, Trau+, and Z3-Trau. Trau uses the first framework presented above and is capable of solving a large class of constraints including transducer and context-free grammar. Trau+ is a later version of Trau and implemented the decision procedure of the weakly-chaining fragment in the over-approximation. Z3-Trau follows the second framework above and uses parametric flat automata for under-approximating the domain of variables. These three string solvers are evaluated on not only existing but also newly generated benchmarks. Evaluation results show that the solvers significantly outperform other state-of-the-art string solvers.
|
|
| 7. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(author)
-
Boosting Constrained Horn Solving by Unsat Core Learning
- 2024
-
In: Verification, Model Checking, and Abstract Interpretation. - : Springer Nature. - 9783031505232 - 9783031505249 ; , s. 280-302
-
Conference paper (peer-reviewed)abstract
- The Relational Hyper-Graph Neural Network (R-HyGNN) was introduced in [1] to learn domain-specific knowledge from program verification problems encoded in Constrained Horn Clauses (CHCs). It exhibits high accuracy in predicting the occurrence of CHCs in counterexamples. In this research, we present an R-HyGNN-based framework called MUSHyperNet. The goal is to predict the Minimal Unsatisfiable Subsets (MUSes) (i.e., unsat core) of a set of CHCs to guide an abstract symbolic model checking algorithm. In MUSHyperNet, we can predict the MUSes once and use them in different instances of the abstract symbolic model checking algorithm. We demonstrate the efficacy of MUSHyperNet using two instances of the abstract symbolic modelchecking algorithm: Counter-Example Guided Abstraction Refinement (CEGAR) and symbolic model-checking-based (SymEx) algorithms. Our framework enhances performance on a uniform selection of benchmarks across all categories from CHC-COMP, solving more problems (6.1% increase for SymEx, 4.1% for CEGAR) and reducing average solving time (13.3% for SymEx, 7.1% for CEGAR).
|
|
| 8. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(author)
-
Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)
- 2019
-
In: Networked Systems. - Cham : Springer Nature. - 9783030312770 - 9783030312763 ; , s. 3-18
-
Conference paper (peer-reviewed)abstract
- We describe at a high-level the main concepts in the Release-Acquire (RA) semantics that is part of the C11 language. Furthermore, we describe the ideas behind an optimal dynamic partial order reduction technique that can be used for systematic analysis of concurrent programs running under RA. This tutorial is based on the material presented in [5], which also contains the formal definitions of all the models, concepts, and algorithms.
|
|
| 9. |
- Abdulla, Parosh Aziz, 1961-, et al.
(author)
-
Parameterized Verification under TSO with Data Types
- 2023
-
In: Tools and Algorithms for the Construction and Analysis of Systems. - : Springer. - 9783031308239 - 9783031308222 ; , s. 588-606
-
Conference paper (peer-reviewed)abstract
- We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type.
|
|
| 10. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(author)
-
Recency-Bounded Verification of Dynamic Database-Driven Systems
- 2016
-
In: PODS'16. - New York, NY, USA : ACM. ; , s. 195-210
-
Conference paper (peer-reviewed)abstract
- We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a DMS modify the current instance of a relational database by adding new elements into the database, deleting tuples from the relations and adding tuples to the relations. The elements which are modified by an action are chosen by (full) first-order queries. DMS is a highly expressive model and can be thought of as a succinct representation of an in finite state relational transition system, in line with similar models proposed in the literature. We propose monadic second order logic (MSO-FO) to reason about sequences of database instances appearing along a run. Unsurprisingly, the linear-time model checking problem of DMS against MSO-FO is undecidable. Towards decidability, we propose under-approximate model checking of DMS, where the under-approximation parameter is the "bound on recency". In a k-recency-bounded run, only the most recent k elements in the current active domain may be modified by an action. More runs can be verified by increasing the bound on recency. Our main result shows that recency-bounded model checking of DMS against MSO-FO is decidable, by a reduction to the satisfiability problem of MSO over nested words.
|
|
