Verification of Parameterized systems by Dynamic Induction on Diagrams

Zohar Manna, Henny Sipma

In this paper we present a visual approach to proving progress properties of parameterized systems using induction on verification diagrams. The inductive hypothesis is represented by an automaton and is based on a state-dependent order on process indices, for increased flexibility. This approach yields more intuitive proofs for progress properties and simpler verification conditions that are more likely to be proved automatically.

Appeared in CAV'99, pp 25-43, LNCS 1633, Springer-Verlag, 1999.

Corrected version: Postscript, PDF. © 1999, Springer Verlag.

Last modified: Thu Mar 29 10:02:32 PST 2001