Verifying Temporal Properties of Reactive Systems: A STeP Tutorial

Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomas Uribe

We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery algorithm for mutual exclusion. We verify the classic two-process algorithm and simple variants, as well as an atomic parameterized version. The methods used include deductive verification rules, verification diagrams, automatic invariant generation, and finite-state model checking and abstraction.

In Formal Methods in System Design, vol 16, pp 227-270, 2000.

Postscript, PDF. © 2000, Kluwer Academic Publishers.


© Henny Sipma / sipma@cs.stanford.edu
Last modified: Thu Mar 29 09:59:07 PST 2001