15–817 Graduate Verification Seminar

15–817 Graduate Verification Seminar

Spring 2013 Semester
Computer Science Department

Course Description

Model Checking is the process of determining whether or not a system model satisfies (is a model of) a property describing desired behavior of the system. Mathematically, system models take the form of state-transition diagrams, while some version of temporal logic is used to describe the desired properties of system executions. A typical property stated in temporal logic is G(req→F ack), indicating that it is invariably the case (G=globally) that a request eventually (F=in the future) triggers an acknowledgment. Two especially noteworthy aspects of Model Checking are: (1) when the system model is finite-state, Model Checking can be performed algorithmically; and (2) when the system is found to violate the property, a counterexample in the form of a system execution is generated that can be used to debug the system model or property.

Announcements

  • Welcome to 15–817!

Lectures

Wednesday from 3:00 to 4:20 pm in GHC 4303.

Contact Information

Instructors

Course Secretary

  • Charlotte Yano
    yan…@cs.cmu.edu
    Office: GHC 9229
    Phone: 412–268–7656