Tutorial on Mechanized Formal Methods
John Rushby
Abstract
This tutorial provides an introduction to several methods of formal
analysis using SRI's theorem proving and model checking tools.
Although it is supported by slides, most of the tutorial consists of a
live demonstration of the various tools and methods applied to a
single, simple example: Lamport's Bakery Algorithm for distributed
mutual exclusion. The idea is to use this single concrete example to
illustrate the style, strengths, and limitations of different methods
of analysis. Although the demonstrations use SRI's tools, the
principles apply to all similar tools.
The tutorial takes 3 to 4 hours and covers the following topics
(though not in this order).
- Finite state methods using
SAL
File for this example:
smallbakery.sal
- Finite-state model checking by explicit state enumeration
(sal-model-checker, sal-viewer)
- Finite-state model checking by symbolic methods using BDDs
(sal-smc, sal-path-finder, sal-sim)
- Finite-state bounded model checking by symbolic methods using SAT solvers
(sal-bmc)
- Finite-state k-induction using SAT solvers
(sal-bmc -i)
- Interactive Theorem Proving using
PVS
Files for this example:
transitions.pvs ,
bakery.pvs ,
absbakery.sal ,
bakery.prf (not for human consumption),
transitions.prf (not for human consumption)
- Verification by interactive theorem proving using inductive invariance
- Verification by interactive theorem proving and finite state model checking using abstraction
- Verification by automated abstraction using decision procedures and finite state model checking
- Automated infinite state methods using SAL with
Yices
File for this example:
bakery.sal
- Infinite-state bounded model checking by symbolic methods using decision procedures
(sal-inf-bmc)
- Infinite-state k-induction using decision procedures
(sal-inf-bmc -i)
If you would like to see an example of SAL applied to
a cryptographic protocol, please see this note regarding the well-known
Needham Schroeder protocol, and for fault tolerance please see
this tutorial on the
OM(1)
algorithm for Byzantine Agreement.
Slides
pdf
or
crude ascii (for your Palm Pilot)
Having trouble reading our papers?
Return to the John Rushby's papers
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page