Welcome to 15-819:

Specification, Verification, and Model Checking
"Spec and Check!"

The goal of this course will be to teach how to specify software systems precisely, and how to use logic and model-checking tools to verify that the systems meet their specifications. We will focus on formal methods for specifications, and on two of the most successful approaches to verification: Hoare Logic and Temporal Model Checking. Examples will come mainly from software and protocol verification.

Classes held Mondays and Wednesdays 1:30-2:50 in Wean 4615A
Units: 12

Description:

This course will focus on the foundations and applications of formal specification and verification. We will present different specification notations for describing desired system properties and different verification techniques for proving that systems satisfy their specifications. We will cover in detail two of the most successful approaches to verification: Hoare Logic and Temporal Logic Model Checking. We will cover in less detail specification notations and tools for describing and checking constraints on software designs. We will show the benefits of writing formal specifications for large system design and for debugging software. Examples will come mainly from software systems and protocol verification.

Instructor Information:

Clarke Jr, Edmund M.
            WEH 7117, 268-2628
             edmund.clarke@cs

Reynolds, John C.
            WEH 8126, 268-3057
             john.reynolds@cs

Wing, Jeannette M.
            WEH 4220, 268-3068
             wing@cs

Prerequisites:

The course is designed to be mostly self-contained. In particular, a prior logic course is not assumed. Knowledge of programming languages and concurrency (at the undergraduate level) will be helpful. Although Model Checking is useful for hardware verification, no knowledge of computer hardware will be required for this course.

Textbooks:

(1) Logic in Computer Science: Modeling and Reasoning about Systems by
       M. Huth and M. Ryan (required)

(2) Model Checking by E. M. Clarke, Orna Grumberg, and Doron Peled (required)

(3) Using Z: Specification, Refinement, and Proof, J. Woodcock and J.
       Davies (recommended)

Method of Evaluation:

Grading will be based on a set of assignments and a take-home final exam.

Topics to be covered:

  • Propositional logic, Predicate calculus, Natural deduction proofs
  • Simple Hoare logic, Weakest preconditions
  • Hoare logic for arrays and for recursive procedures
  • Shared mutable data structures - separation logic
  • Reasoning about behavioral subtyping - abstraction functions
  • The Davis-Putnam procedure and modern SAT procedures (Grasp, Chaff, etc.)
  • Property specification using Computation Tree Logic (CTL)
  • Concurrency (synchronous and asynchronous models), Fairness
  • Explicit state model checking
  • Binary decision diagrams (BDDs)
  • Symbolic model checking
  • Specification notations for software design
  • Case studies of specifying large software systems
  • Tools for checking software design