| 1. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
On the Separability Problem of String Constraints
- 2020
-
Ingår i: 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference). - Dagstuhl, Germany. - 9783959771603 ; , s. 16:1-16:19
-
Konferensbidrag (refereegranskat)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.
(författare)
-
On the State Reachability Problem for Concurrent Programs Under Power
- 2020
-
Ingår i: Networked Systems - 8th International Conference, {NETYS} 2020, Morocco, Revised Selected Papers. - : Springer Nature Switzerland AG.
-
Konferensbidrag (refereegranskat)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. |
|
|
| 4. |
- Bui, Phi Diep
(författare)
-
On Solving String Constraints
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)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.
|
|
| 5. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(författare)
-
Boosting Constrained Horn Solving by Unsat Core Learning
- 2024
-
Ingår i: Verification, Model Checking, and Abstract Interpretation. - : Springer Nature. - 9783031505232 - 9783031505249 ; , s. 280-302
-
Konferensbidrag (refereegranskat)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).
|
|
| 6. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(författare)
-
Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)
- 2019
-
Ingår i: Networked Systems. - Cham : Springer Nature. - 9783030312770 - 9783030312763 ; , s. 3-18
-
Konferensbidrag (refereegranskat)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.
|
|
| 7. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(författare)
-
Recency-Bounded Verification of Dynamic Database-Driven Systems
- 2016
-
Ingår i: PODS'16. - New York, NY, USA : ACM. ; , s. 195-210
-
Konferensbidrag (refereegranskat)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.
|
|
| 8. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(författare)
-
The Decidability of Verification under PS 2.0
- 2021
-
Ingår i: Programming Languages And Systems, ESOP 2021. - Cham : Springer Nature. - 9783030720193 - 9783030720186 ; , s. 1-29
-
Konferensbidrag (refereegranskat)abstract
- We consider the reachability problem for finite-state multi-threaded programs under the promising semantics (PS 2.0) of Lee et al., which captures most common program transformations. Since reachability is already known to be undecidable in the fragment of PS 2.0 with only release-acquire accesses (PS 2.0-ra), we consider the fragment with only relaxed accesses and promises (PS 2.0-rlx). We show that reachability under PS 2.0-rlx is undecidable in general and that it becomes decidable, albeit non-primitive recursive, if we bound the number of promises. Given these results, we consider a bounded version of the reachability problem. To this end, we bound both the number of promises and of "view-switches", i.e., the number of times the processes may switch their local views of the global memory. We provide a code-to-code translation from an input program under PS 2.0 (with relaxed and release-acquire memory accesses along with promises) to a program under SC, thereby reducing the bounded reachability problem under PS 2.0 to the bounded context-switching problem under SC. We have implemented a tool and tested it on a set of benchmarks, demonstrating that typical bugs in programs can be found with a small bound.
|
|
| 9. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Consistency and Persistency in Program Verification : Challenges and Opportunities
- 2022
-
Ingår i: Principles of Systems Design. - Cham : Springer. - 9783031223365 - 9783031223372 ; , s. 494-510
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- We consider the verification of concurrent programs and, in particular, the challenges that arise because modern platforms only guarantee weak semantics, i.e., semantics that are weaker than the classical Sequential Consistency (SC). We describe two architectural concepts that give rise to weak semantics, namely weak consistency and weak persistency. The former defines the order in which operations issued by a given process become visible to the rest of the processes. The latter prescribes the order in which data becomes persistent. To deal with the extra complexity in program behaviors that arises due to weak semantics, we propose translating the program verification problem under weak semantics to SC. The main principle is to augment the program with a set of (unbounded) data structures that guarantee the equivalence of the source program’s behavior under the weak semantics with the augmented program’s behavior under the SC semantics. Such an equivalence opens the door to leverage, albeit in a non-trivial manner, the rich set of techniques that we have developed over the years for program verification under the SC semantics. We illustrate the framework’s potential by considering the persistent version of the well-known Total Store Order semantics. We show that we can capture the program behaviors on such a platform using a finite set of unbounded monotone FIFO buffers. The use of monotone FIFO buffers allows the use of the well-structured-systems framework to prove the decidability of the reachability problem.
|
|
| 10. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Deciding Reachability under Persistent x86-TSO
- 2021
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 5
-
Tidskriftsartikel (refereegranskat)abstract
- We address the problem of verifying the reachability problem in programs running under the formal model Px86 defined recently by Raad et al. in POPL'20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.
|
|
