Technical Report 2007-014

Parameterized Verification of Infinite-state Processes with Global Conditions

Parosh Aziz Abdulla, Giorgio Delzanno, and Ahmed Rezine

April 2007

We present a simple and effective approximated backward reachability algorithm for parameterized systems with existentially and universally quantified global conditions. The individual processes operate on unbounded local variables ranging over the natural numbers. In addition, processes may communicate via broadcast, rendez-vous and shared variables. We apply the algorithm to verify mutual exclusion for complex protocols such as Lamport's bakery algorithm both with and without atomicity conditions, a distributed version of the bakery algorithm, and Ricart-Agrawala's distributed mutual exclusion algorithm.

Note: A short version of this paper will appear in the proceedings of Computer Aided Verification (CAV) 2007.

Available as PDF (323 kB, no cover)

Download BibTeX entry.