STeP: The Stanford Temporal Prover
Tutorial

Manual Session Editor Proof Editor Diagram Editor


Basic Tutorial

A basic tutorial is provided that demonstrates how to verify some properties of a 2-process version of Lamport's Bakery algorithm.

Feature-specific tutorials

Tutorials on other topics can be accessed by clicking on the highlighted areas in the STeP diagram below.

Reactive systems Real-time systems Hybrid systems Fair transition systems Temporal specifications Modularity Abstraction Decision procedures Simplifier Verification diagrams Symbolic Model checking Explicit state model checking Interactive verification

Last modified: Wed Jul 1 09:17:45 PDT 1998