Case studies

Papers

• Our 1994 technical report describes a number of examples, including a parameterized ring-arbiter and Szymanski's N-process mutual exclusion algorithm.

• Jonathan Ostroff from York university in Canada has used STeP to verify systems in the TTM/RTTL framework.

• Nikolaj Bjørner, Zohar Manna and Uri Lerner. Deductive verification of parameterized fault-tolerant systems: A case study . Presented at ICTL 97.

• Nikolaj Bjørner, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Deductive Verification of Real-time Systems Using STeP . Presented at ARTS 97.

On-line material

• A ring based leader-election algorithm By Calogero Zarba.
• Model checking the Needham-Schroeder protocol By Calogero Zarba.
• A round-robin Bakery algorithm By Calogero Zarba.
• Verification of a DLX pipeline (a benchmark for congruence closure).

Notes

• A demarcation protocol By Jeff Kamerer.
• A split transaction bus By Jeff Kamerer.
• The Ricard-Agrawala protocol By Jeff Kamerer.