Tutorial on Mechanized Formal Methods

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)