# 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

- Prof. Edmund M. Clarke

emc…@cs.cmu.edu

Office: GHC 9231

Phone: (412) 268–2628

Office hours: By appointment

### Course Secretary

- Charlotte Yano

yan…@cs.cmu.edu

Office: GHC 9229

Phone: 412–268–7656