| 1. |
- 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).
|
|
| 2. |
|
|
| 3. |
- Abdulla, Parosh Aziz, 1961-, et al.
(författare)
-
Parameterized verification under TSO is PSPACE-complete
- 2020
-
Ingår i: Proceedings of the ACM on Programming Languages. - New York, NY, USA : Association for Computing Machinery (ACM). - 2475-1421. ; 4:POPL, s. 26:1-26:29
-
Tidskriftsartikel (refereegranskat)abstract
- We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and write operations. We show that the reachability problem for a system consisting of an arbitrary number of identical processes is PSPACE-complete. We prove that the complexity is reduced to polynomial time if the processes are not allowed to read the initial values of the variables in the memory. When the processes are allowed to perform atomic read-modify-write operations, the reachability problem has a non-primitive recursive complexity.
|
|
| 4. |
- 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.
|
|
| 5. |
- 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.
|
|
| 6. |
- 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.
|
|
| 7. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Efficient Handling of String-Number Conversion
- 2020
-
Ingår i: PLDI 2020. - New York, NY, USA : ACM. - 9781450376136 ; , s. 943-957
-
Konferensbidrag (refereegranskat)abstract
- String-number conversion is an important class of constraints needed for the symbolic execution of string-manipulating programs. In particular solving string constraints with string-number conversion is necessary for the analysis of scripting languages such as JavaScript and Python, where string-number conversion is a part of the definition of the core semantics of these languages. However, solving this type of constraint is very challenging for the state-of-the-art solvers. We propose in this paper an approach that can efficiently support both string-number conversion and other common types of string constraints. Experimental results show that it significantly outperforms other state-of-the-art tools on benchmarks that involves string-number conversion.
|
|
| 8. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
On the Formalization of Decentralized Contact Tracing Protocols
- 2020
-
Ingår i: Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Bolzano Summer of Knowledge 2020 {(BOSK} 2020), September 25, 2020. - : CEUR-WS.org. ; , s. 65-70
-
Konferensbidrag (refereegranskat)abstract
- We present a preliminary formalization based on transition systems of decentralized contact tracing protocols for smart devices equipped with Bluetooth trasmitters. In our model the behaviour of individual users, via their app, is modelled as a timed automata with a local unbounded memory. Protocol configurations consist of the current state of a shared server and a finite set of local states containing the states of individual users. The transition system models the interaction between devices in the same physical location and between a sigle device and the shared server. In the paper we address different research directions concerning semi-automated verification based on automated reasoning tools of the considered class of protocols, theoretical issues related to the expressiveness of the resulting class of formal models, and data-driven analysis of the logs collected on the server as well as on user devices.
|
|
| 9. |
- 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.
|
|
| 10. |
- 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.
|
|
