| 1. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Monotonic abstraction for programs with dynamic memory heaps
- 2008
-
In: Computer Aided Verification. - Berlin : Springer-Verlag. ; , s. 341-354
-
Conference paper (peer-reviewed)abstract
- We propose a new approach for automatic verification of programs with dynamic heap manipulation. The method is based on symbolic (backward) reachability analysis using upward-closed sets of heaps w.r.t. an appropriate preorder on graphs. These sets are represented by a finite set of minimal graph patterns corresponding to a set of bad configurations. We define an abstract semantics for the programs which is monotonic w.r.t. the preorder. Moreover, we prove that our analysis always terminates by showing that the preorder is a well-quasi ordering. Our results are presented for the case of programs with 1-next selector. We provide experimental results showing the effectiveness of our approach.
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
|
|
| 5. |
|
|
| 6. |
- Abdulla, Aziz, et al.
(author)
-
Monotonic Abstraction : on Efficient Verification of Parameterized Systems
- 2009
-
In: International Journal of Foundations of Computer Science. - 0129-0541. ; 20:5, s. 779-801
-
Journal article (peer-reviewed)abstract
- We introduce the simple and efficient method of monotonic abstraction to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables over finite domains. The method of monotonic abstraction derives an over-approximation of the induced transition system that allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype that works well on several mutual exclusion algorithms and cache coherence protocols
|
|
| 7. |
|
|
| 8. |
- Abdulla, Parosh Aziz, et al.
(author)
-
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
- 2013
-
In: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin Heidelberg.
-
Conference paper (peer-reviewed)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.
|
|
| 9. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Automatic fence insertion in integer programs via predicate abstraction
- 2012
-
In: Static Analysis. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642331244 - 9783642331251 ; , s. 164-180
-
Conference paper (peer-reviewed)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. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Automatic verification of directory-based consistency protocols with graph constraints
- 2011
-
In: International Journal of Foundations of Computer Science. - 0129-0541. ; 22:4, s. 761-782
-
Journal article (peer-reviewed)abstract
- We propose a symbolic verification method for directory-based consistency protocols working for an arbitrary number of controlled resources and competing processes. We use a graph-based language to specify in a uniform way both client/server interaction schemes and manipulation of directories that contain the access rights of individual clients. Graph transformations model the dynamics of a given protocol. Universally quantified conditions defined on the labels of edges incident to a given node are used to model inspection of directories, invalidation loops and integrity conditions. Our verification procedure computes an approximated backward reachability analysis by using a symbolic representation of sets of configurations. Termination is ensured by using the theory of well-quasi orderings.
|
|
