| 1. |
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
- 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
|
|
| 5. |
|
|
| 6. |
- Abdulla, Parosh Aziz, 1961-, et al.
(author)
-
A classification of the expressive power of well-structured transition systems
- 2011
-
In: Information and Computation. - : Elsevier BV. - 0890-5401 .- 1090-2651. ; 209:3, s. 248-279
-
Journal article (peer-reviewed)abstract
- We compare the expressive power of a class of well-structured transition systems that includes relational automata (extensions of), Petri nets, lossy channel systems, constrained multiset rewriting systems, and data nets. For each one of these models we study the class of languages generated by labeled transition systems describing their semantics. We consider here two types of accepting conditions: coverability and reachability of a fixed a priori configuration. In both cases we obtain a strict hierarchy in which constrained multiset rewriting systems is the most expressive model.
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(author)
-
A general approach to partial order reductions in symbolic verification
- 1998
-
In: Computer Aided Verification. - 9783540646082 - 9783540693390 ; , s. 379-390
-
Conference paper (peer-reviewed)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.
|
|
| 8. |
- Abdulla, Parosh Aziz, et al.
(author)
-
A load-buffer semantics for total store ordering
- 2018
-
In: Logical Methods in Computer Science. - 1860-5974. ; 14:1
-
Journal article (peer-reviewed)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.
|
|
| 9. |
|
|
| 10. |
|
|
