| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
A general approach to partial order reductions in symbolic verification
- 1998
-
Ingår i: Computer Aided Verification. - 9783540646082 - 9783540693390 ; , s. 379-390
-
Konferensbidrag (refereegranskat)abstract
- The purpose of partial-order reduction techniques is to avoid exploring several interleavings of independent transitions when model checking the temporal properties of a concurrent system. The purpose of symbolic verification techniques is to perform basic manipulations on sets of states rather than on individual states. We present a general method for applying partial order reductions to improve symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation.We show how our method can be applied to several models of infinite-state systems: systems communicating over unbounded lossy FIFO channels, and unsafe (infinite-state Petri Nets. We show by a simple example how partial order reduction can significantly speed up symbolic backward analysis of Petri Nets.
|
|
| 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. |
|
|
| 5. |
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
- 2013
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin Heidelberg.
-
Konferensbidrag (refereegranskat)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which rely on subtle dependen- cies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded num- ber of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state au- tomata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verifica- tion, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have imple- mented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 7. |
|
|
| 8. |
|
|
| 9. |
- 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.
|
|
| 10. |
|
|
