This course is a graduate level research seminar on automatic verification techniques for concurrent, reactive, and real-time programs. It was last taught in the spring of 1996, but different topics will be covered this semester
The prerequisites for the course are minimal--basic knowledge of elementary logic and automata theory. In particular, students who did not take the course in the spring should have no difficulty understanding the material that is presented this semester. Students taking the class for graduate credit will be asked to prepare a short project and give one or two lectures. Auditors are also welcomed.
Detailed Course Description: Logical errors in hardware controllers, communication protocols, and real-time programs are becoming an increasingly important problem. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. The most widely used method for verifying such systems is based on extensive simulation and can easily miss significant errors when the program is very complicated.
Many of these programs can be viewed as having only a finite number of states. When this is the case, an alternative verification technique called "model checking" may be used. In this approach specifications are expressed by automata or temporal logic formulas, and programs are modeled as state transition systems. An efficient search procedure is used to determine automatically if the specifications are satisfied by the transition system. The technique has been used in the past to find subtle errors in a number of non-trivial designs. Recently, the size of the state transition systems that can be verified by model checking methods has increased dramatically. By representing transition relations implicitly using Binary Decision Diagrams (BDDs), it has become possible to check some examples with more than 10^100 states!