| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
A load-buffer semantics for total store ordering
- 2018
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 14:1
-
Tidskriftsartikel (refereegranskat)abstract
- We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove the correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes. In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO semantics that is more amenable to efficient algorithmic verification and for the extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows obtaining a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Adding time to pushdown automata
- 2012
-
Ingår i: Quantities in Formal Methods. ; , s. 1-16
-
Konferensbidrag (refereegranskat)
|
|
| 3. |
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Automatic fence insertion in integer programs via predicate abstraction
- 2012
-
Ingår i: Static Analysis. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642331244 - 9783642331251 ; , s. 164-180
-
Konferensbidrag (refereegranskat)abstract
- We propose an automatic fence insertion and verification framework for concurrent programs running under relaxed memory. Unlike previous approaches to this problem, which allow only variables of finite domain, we target programs with (unbounded) integer variables. The problem is difficult because it has two different sources of infiniteness: unbounded store buffers and unbounded integer variables. Our framework consists of three main components: (1) a finite abstraction technique for the store buffers, (2) a finite abstraction technique for the integer variables, and (3) a counterexample guided abstraction refinement loop of the model obtained from the combination of the two abstraction techniques. We have implemented a prototype based on the framework and run it successfully on all standard benchmarks together with several challenging examples that are beyond the applicability of existing methods.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Budget-bounded model-checking pushdown systems
- 2014
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 45:2, s. 273-301
-
Tidskriftsartikel (refereegranskat)abstract
- We address the verification problem for concurrent programs modeled as multi-pushdown systems (MPDS). In general, MPDS are Turing powerful and hence come along with undecidability of all basic decision problems. Because of this, several subclasses of MPDS have been proposed and studied in the literature (Atig et al. in LNCS, Springer, Berlin, 2005; La Torre et al. in LICS, IEEE, 2007; Lange and Lei in Inf Didact 8, 2009; Qadeer and Rehof in TACAS, LNCS, Springer, Berlin, 2005). In this paper, we propose the class of bounded-budget MPDS, which are restricted in the sense that each stack can perform an unbounded number of context switches only if its depth is below a given bound, and a bounded number of context switches otherwise. We show that the reachability problem for this subclass is Pspace-complete and that LTL-model-checking is Exptime-complete. Furthermore, we propose a code-to-code translation that inputs a concurrent program and produces a sequential program such that running under the budget-bounded restriction yields the same set of reachable states as running . Moreover, detecting (fair) non-terminating executions in can be reduced to LTL-Model-Checking of . By leveraging standard sequential analysis tools, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our translation.
|
|
| 6. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Chain-Free String Constraints
- 2019
-
Ingår i: Automated Technology for Verification and Analysis. - Cham : Springer. - 9783030317836 - 9783030317843 ; , s. 277-293
-
Konferensbidrag (refereegranskat)abstract
- We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. 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. We have developed a prototype implementation of our new decision procedure, and integrated it into in an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. Our experimental results show the competitiveness and accuracy of the new framework.
|
|
| 7. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Complexity of reachability for data-aware dynamic systems
- 2018
-
Ingår i: Proc. 18th International Conference on Application of Concurrency to System Design. - : IEEE Computer Society. - 9781538670132 ; , s. 11-20
-
Konferensbidrag (refereegranskat)abstract
- A formal model called database manipulating systems was introduced to model data-aware dynamic systems. Its semantics is given by an infinite labelled transition systems where a label can be an unbounded relational database. Reachability problem is undecidable over schemas consisting of either a binary relation or two unary relations. We study the reachability problem under schema restrictions and restrictions on the query language. We provide tight complexity bounds for different combinations of schema and query language, by reductions to/from standard formalism of infinite state systems such as Petri nets and counter systems. Our reductions throw light into the connections between these two seemingly unrelated models.
|
|
| 8. |
|
|
| 9. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Context-bounded analysis for POWER
- 2017
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer. - 9783662545799 ; , s. 56-74
-
Konferensbidrag (refereegranskat)abstract
- We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis initiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs (supposed to be running under the classical SC model). To that end, we first introduce a new notion of context-bounding that is suitable for reasoning about computations under POWER, which generalizes the one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a polynomial size reduction of the context-bounded state reachability problem under POWER to the same problem under SC: Given an input concurrent program P, our method produces a concurrent program P' such that, for a fixed number of context switches, running P' under SC yields the same set of reachable states as running P under POWER. The generated program P' contains the same number of processes as P and operates on the same data domain. By leveraging the standard model checker CBMC, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our approach.
|
|
| 10. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Counter-Example Guided Fence Insertion under TSO
- 2012
-
Ingår i: TACAS 2012. - Berlin, Heidelberg : Springer. - 9783642287558 - 9783642287565
-
Konferensbidrag (refereegranskat)abstract
- We give a sound and complete fence insertion procedure for concurrentfinite-state programs running under the classical TSO memory model. Thismodel allows “write to read” relaxation corresponding to the addition of an unboundedstore buffer between each processor and the main memory. We introducea novel machine model, called the Single-Buffer (SB) semantics, and show thatthe reachability problem for a program under TSO can be reduced to the reachabilityproblem under SB. We present a simple and effective backward reachabilityanalysis algorithm for the latter, and propose a counter-example guided fence insertionprocedure. The procedure is augmented by a placement constraint thatallows the user to choose places inside the program where fences may be inserted.For a given placement constraint, we automatically infer all minimal setsof fences that ensure correctness. We have implemented a prototype and run itsuccessfully on all standard benchmarks together with several challenging examplesthat are beyond the applicability of existing methods.
|
|
| 11. |
|
|
| 12. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Data Communicating Processes with Unreliable Channels
- 2016
-
Ingår i: Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016). - 9781450343916 ; , s. 166-175
-
Konferensbidrag (refereegranskat)abstract
- We extend the classical model of lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.
|
|
| 13. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Dense-Timed Pushdown Automata
- 2012
-
Ingår i: Proc. 27th ACM/IEEE Symposium on Logic in Computer Science. - : IEEE Computer Society. - 9780769547695 ; , s. 35-44
-
Konferensbidrag (refereegranskat)abstract
- We propose a model that captures the behavior of real-time recursive systems. To that end, we introduce dense-timed pushdown automata that extend the classical models of pushdown automata and timed automata, in the sense that the automaton operates on a finite set of real-valued clocks, and each symbol in the stack is equipped with a real-valued clock representing its "age". The model induces a transition system that is infinite in two dimensions, namely it gives rise to a stack with an unbounded number of symbols each of which with a real-valued clock. The main contribution of the paper is an EXPTIME-complete algorithm for solving the reachability problem for dense-timed pushdown automata.
|
|
| 14. |
- 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.
|
|
| 15. |
|
|
| 16. |
- Abdulla, Parosh Aziz, 1961-, et al.
(författare)
-
Flatten and Conquer : A Framework for Efficient Analysis of String Constraints
- 2017
-
Ingår i: SIGPLAN notices. - New York, NY, USA : ACM. - 0362-1340 .- 1558-1160. - 9781450349888 ; 52:6, s. 602-617, s. 602-617
-
Tidskriftsartikel (refereegranskat)abstract
- We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under-and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.
|
|
| 17. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Infinite-state energy games
- 2014
-
Ingår i: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014. - New York : ACM Press. - 9781450328869
-
Konferensbidrag (refereegranskat)abstract
- Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this.We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata.Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.
|
|
| 18. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
- 2013
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642367410 - 9783642367427 ; , s. 530-536
-
Konferensbidrag (refereegranskat)abstract
- We introduce MEMORAX, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory models. The verification task is non-trivial as it involves exploring state spaces of arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables, the sizes of the store buffers could grow unboundedly, and hence the state spaces that need to be explored could be of infinite size. In addition, MEMORAX in- corporates an interpolation based CEGAR loop to make possible the verification of control state reachability for concurrent programs involving integer variables. The reachability procedure is used to automatically compute possible memory fence placements that guarantee the unreachability of bad control states under TSO. In fact, for programs only involving finite range variables and running on TSO, the fence insertion functionality is complete, i.e., it will find all minimal sets of memory fence placements (minimal in the sense that removing any fence would result in the reachability of the bad control states). This makes MEMORAX the first freely available, open source, push-button verification and fence insertion tool for programs running under TSO with integer variables.
|
|
| 19. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Mending fences with self-invalidation and self-downgrade
- 2018
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 14:1
-
Tidskriftsartikel (refereegranskat)abstract
- Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction reordering, thus causing extra program behaviors that are often not intended by the programmers. We propose a novel formal model that captures the semantics of programs running under such protocols, and features a set of fences that interact with the coherence layer. Using the model, we design an algorithm to analyze the reachability and check whether a program satisfies a given safety property with the current set of fences. We describe a method for insertion of optimal sets of fences that ensure correctness of the program under such protocols. The method relies on a counter-example guided fence insertion procedure. One feature of our method is that it can handle a variety of fences (with different costs). This diversity makes optimization more difficult since one has to optimize the total cost of the inserted fences, rather than just their number. To demonstrate the strength of our approach, we have implemented a prototype and run it on a wide range of examples and benchmarks. We have also, using simulation, evaluated the performance of the resulting fenced programs.
|
|
| 20. |
|
|
| 21. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Multi-Pushdown Systems with Budgets
- 2012
-
Ingår i: Formal Methods in Computer-Aided Design. ; , s. 24-33
-
Konferensbidrag (refereegranskat)
|
|
| 22. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Norn: An SMT Solver for String Constraints
- 2015
-
Ingår i: COMPUTER AIDED VERIFICATION, PT I. - Cham : SPRINGER-VERLAG BERLIN. - 9783319216904 - 9783319216898 ; , s. 462-469
-
Konferensbidrag (refereegranskat)abstract
- We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.
|
|
| 23. |
- 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.
|
|
| 24. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Precise and sound automatic fence insertion procedure under PSO
- 2015
-
Ingår i: Networked Systems. - Cham : Springer. - 9783319268491 ; , s. 32-47
-
Konferensbidrag (refereegranskat)abstract
- We give a sound and complete procedure for fence insertion for concurrent finite-state programs running under the PSO memory model. This model allows ''write to read'' and ''write-to-write'' relaxations corresponding to the addition of an unbounded store buffers between processors and the main memory. We introduce a novel machine model, called the Hierarchical Single-Buffer (HSB) semantics, and show that the reachability problem for a program under PSO can be reduced to the reachability problem under HSB. We present a simple and effective backward reachability analysis algorithm for the latter, and propose a counter-example guided fence insertion procedure. The procedure infers automatically a minimal set of fences that ensure correctness of the program. We have implemented a prototype and run it successfully on all standard benchmarks, together with several challenging examples.
|
|
| 25. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Push-down automata with gap-order constraints
- 2013
-
Ingår i: Fundamentals of Software Engineering. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642402128 ; , s. 199-216
-
Konferensbidrag (refereegranskat)
|
|
| 26. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Reachability in database-driven systems with numerical attributes under recency bounding
- 2019
-
Ingår i: PODS '19. - New York, NY, USA : ACM Press. - 9781450362276 ; , s. 335-352
-
Konferensbidrag (refereegranskat)abstract
- A prominent research direction of the database theory community is to develop techniques for verification of database-driven systems operating over relational and numerical data. Along this line, we lift the framework of database manipulating systems [3] which handle relational data to also accommodate numerical data and the natural order on them. We study an under-approximation called recency bounding under which the most basic verification problem-reachability, is decidable. Even under this under-approximation the reachability space is infinite in multiple dimensions - owing to the unbounded sizes of the active domain, the unbounded numerical domain it has access to, and the unbounded length of the executions. We show that, nevertheless, reachability is ExpTime complete. Going beyond reachability to LTL model checking renders verification undecidable.
|
|
| 27. |
- 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.
|
|
| 28. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Replacing store buffers by load buffers in TSO
- 2018
-
Ingår i: Verification and Evaluation of Computer and Communication Systems. - Cham : Springer. - 9783030003586 - 9783030003593 ; , s. 22-28
-
Konferensbidrag (refereegranskat)abstract
- We consider the weak memory model of Total Store Ordering (TSO). In the classical definition of TSO, an unbounded buffer is inserted between each process and the shared memory. The buffers contains pending store operations of the processes. We introduce a new model where we replace the store buffers by load buffers. In contrast to the classical model, the buffers now contain load operations. We show that the models have equivalent behaviors in the sense that the processes reach identical sets of states when the input program is run under the two models.
|
|
| 29. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for POWER
- 2016
-
Ingår i: Computer Aided Verification. - Cham : Springer. - 9783319415390 - 9783319415406 ; , s. 134-156
-
Konferensbidrag (refereegranskat)abstract
- We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to the axiomatic model of POWER from [8]. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.
|
|
| 30. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for TSO and PSO
- 2015
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783662466803 ; , s. 353-367
-
Konferensbidrag (refereegranskat)
|
|
| 31. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for TSO and PSO
- 2017
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 54:8, s. 789-818
-
Tidskriftsartikel (refereegranskat)
|
|
| 32. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
String Constraints for Verification
- 2014
-
Ingår i: <em>26th International Conference on Computer Aided Verification (CAV 2014), Vienna, Austria, Jul. 9-12, 2014.</em>. - Berlin : Springer. - 9783319088662 - 9783319088679 ; , s. 150-166
-
Konferensbidrag (refereegranskat)abstract
- We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs that are beyond the reach of existing methods.
|
|
| 33. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
String Constraints for Verification
- 2014
-
Ingår i: Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings. - Cham : Springer. - 9783319088662 ; , s. 150-166
-
Konferensbidrag (refereegranskat)abstract
- We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs that are beyond the reach of existing methods.
|
|
| 34. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
The benefits of duality in verifying concurrent programs under TSO
- 2016
-
Ingår i: 27th International Conference on Concurrency Theory. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783959770170 ; , s. 5:1-15
-
Konferensbidrag (refereegranskat)abstract
- We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove the correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes.In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO semantics that is more amenable to efficient algorithmic verification and for the extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows obtaining a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.
|
|
| 35. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
The Best of Both Worlds: Trading efficiency and optimality in fence insertion for TSO
- 2015
-
Ingår i: Programming Languages and Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783662466681 ; , s. 308-332
-
Konferensbidrag (refereegranskat)abstract
- We present a method for automatic fence insertion in concurrent programs running under weak memory models that provides the best known trade-off between efficiency and optimality. On the one hand, the method can efficiently handle complex aspects of program behaviors such as unbounded buffers and large numbers of processes. On the other hand, it is able to find small sets of fences needed for ensuring correctness of the program. To this end, we propose a novel notion of correctness, called persistence, that compares the behavior of the program under the weak memory semantics with that under the classical interleaving (SC) semantics. We instantiate our framework for the Total Store Ordering (TSO) memory model, and give an algorithm that reduces the fence insertion problem under TSO to the reachability problem for programs running under SC. Furthermore, we provide an abstraction scheme that substantially increases scalability to large numbers of processes. Based on our method, we have implemented a tool and run it successfully on a wide range benchmarks.
|
|
| 36. |
- 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.
|
|
| 37. |
|
|
| 38. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Timed lossy channel systems
- 2012
-
Ingår i: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783939897477 ; , s. 374-386
-
Konferensbidrag (refereegranskat)
|
|
| 39. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Timed Lossy Channel Systems
- 2012
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Lossy channel systems are a classical model with applications ranging from the modeling of communication protocols to programs running on weak memory models. All existing work assume that messages traveling inside the channels are picked from a finite alphabet. In this paper, we extend the model by assuming that each message is equipped with a clock representing the age of the message, thus obtaining the model of \emphTimed Lossy Channel Systems (TLCS). The main contribution of the paper is to show that the control state reachability problem is decidable for TLCS.
|
|
| 40. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
TRAU : SMT solver for string constraints
- 2018
-
Ingår i: PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD). - : IEEE. - 9780983567882 ; , s. 165-169
-
Konferensbidrag (refereegranskat)abstract
- We introduce TRAU, an SMT solver for an expressive constraint language, including word equations, length constraints, context-free membership queries, and transducer constraints. The satisfiability problem for such a class of constraints is in general undecidable. The key idea behind TRAU is a technique called flattening, which searches for satisfying assignments that follow simple patterns. TRAU implements a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The approximations are refined in an automatic manner by information flow between the two modules. The technique implemented by TRAU can handle a rich class of string constraints and has better performance than state-of-the-art string solvers.
|
|
| 41. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Universal safety for timed Petri nets is PSPACE-complete
- 2018
-
Ingår i: 29th International Conference on Concurrency Theory. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783959770873 ; , s. 6:1-15
-
Konferensbidrag (refereegranskat)
|
|
| 42. |
|
|
| 43. |
|
|
| 44. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verification of Directed Acyclic Ad Hoc Networks
- 2013
-
Ingår i: Formal Techniques for Distributed Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642385919 ; , s. 193-208
-
Konferensbidrag (refereegranskat)
|
|
| 45. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verification of Dynamic Register Automata
- 2014
-
Ingår i: Leibniz International Proceedings in Informatics.
-
Konferensbidrag (refereegranskat)abstract
- We consider the verification problem for Dynamic Register Automata (Dra). Dra extend classical register automata by process creation. In this setting, each process is equipped with a finite number of registers in which the process IDs of other processes can be stored. A process can communicate with processes whose IDs are stored in its registers and can send them the content of its registers. The state reachability problem asks whether a Dra reaches a configuration where at least one process is in an error state. We first show that this problem is in general undecidable. This result holds even when we restrict the analysis to configurations where the maximal length of the simple paths in their underlying (un)directed communication graphs are bounded by some constant. Then we introduce the model of degenerative Dra which allows non-deterministic reset of the registers. We prove that for every given Dra, its corresponding degenerative one has the same set of reachable states. While the state reachability of a degenerative Dra remains undecidable, we show that the problem becomes decidable with nonprimitive-recursive complexity when we restrict the analysis to strongly bounded configurations, i.e. configurations whose underlying undirected graphs have bounded simple paths. Finally, we consider the class of strongly safe Dra, where all the reachable configurations are assumed to be strongly bounded. We show that for strongly safe Dra, the state reachability problem becomes decidable.
|
|
| 46. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Verification of programs under the release-acquire semantics
- 2019
-
Ingår i: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450367127 ; , s. 1117-1132
-
Konferensbidrag (refereegranskat)abstract
- We address the verification of concurrent programs running under the release-acquire (RA) semantics. We show that the reachability problem is undecidable even in the case where the input program is finite-state. Given this undecidability, we follow the spirit of the work on context-bounded analysis for detecting bugs in programs under the classical SC model, and propose an under-approximate reachability analysis for the case of RA. To this end, we propose a novel notion, called view-switching, and provide a code-to-code translation from an input program under RA to a program under SC. This leads to a reduction, in polynomial time, of the bounded view-switching reachability problem under RA to the bounded context-switching problem under SC. We have implemented a prototype tool VBMC and tested it on a set of benchmarks, demonstrating that many bugs in programs can be found using a small number of view switches.
|
|
| 47. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Verification of timed asynchronous programs
- 2018
-
Ingår i: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783959770934 ; , s. 8:1-16
-
Konferensbidrag (refereegranskat)
|
|
| 48. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
What's decidable about availability languages?
- 2015
-
Ingår i: Proc. 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783939897972 ; , s. 192-205
-
Konferensbidrag (refereegranskat)
|
|
| 49. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Zenoness for Timed Pushdown Automata
- 2014
-
Ingår i: Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013.. ; , s. -47
-
Konferensbidrag (refereegranskat)abstract
- Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clocks and the age of the topmost symbol. Therefore, dense-timed pushdown automata subsume both pushdown automata and timed automata. We have previously shown that the reachability problem for this model is decidable. In this paper, we study the zenoness problem and show that it is EXPTIME-complete.
|
|
| 50. |
- 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.
|
|
