Tutorial on Mechanized Formal Methods

John Rushby


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).

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.


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