CS395T Model Checking

Overview

Temporal Logic model checking is a method of automatically verifying the correctness of (finite state) concurrent systems. The fixpoint characterizations of temporal operators together with the Tarski-Knaster theorem provide a simple but efficient and expressive means of searching the global state graph of a concurrent system to determine if it is a model of the temporal logic correctness specification. The method was originally developed in academia but finds increasingly widespread industrial application in such areas as microprocessor design and communication protocol analysis. Commercially developed model checkers are now appearing in the market place. Pre-requisites: Some knowledge of temporal logic OR permission of instructor (emerson@cs.utexas.edu; 471-9537; Tay 3.130 TTh4p)

Topics:

• Temporal logic review.
• State explosion amelioration.
  • "Symbolic" BDD-based representations.
  • Symmetry reduction.
  • Partial order reduction.
  • On-the-fly algorithms.
  • Abstractions.
• Compositional model checking.
• Real-time model checking.
• Beyond model checking?

Pre-requisites: Some knowledge of temporal logic OR permission of instructor.

Administrative Information

• Unique Number: 49450
• Meeting Time/Place: Tu 6:30-9, TAY 3.144
• Instructor: E. Allen Emerson
• Office Hours: TBA.
• Classlist with e-mail.

Readings

• E. Allen Emerson, Temporal and Modal Logic. In J. van Leeuwen, Ed., Handbook of Theoretical Computer Science, Vol. B, Elsevier, 1990.
• E. Allen Emerson, Model Checking and the Mu-Calculus.
• E. Allen Emerson, Automated Temporal Reasoning about Reactive Systems.

Projects

• Click here for suggested tools and the current assignment.

Links

• Formal methods page at Oxford.
• Formal methods page at CMU.
• Hardware verification page at Stanford.