Synopsis

  • Course number: CS 7485
  • Class times: Wed & Fri 2:00pm -- 3:40pm
  • Class location: room 166, West Village H
  • Instructor: Thomas Wahl
  • Office hours: after each class session, room 344, 202 West Village H

Course contents

Formal verification (FV) is concerned with the use of methods borrowed from discrete mathematics and logic to analyze "mechanically" (i.e., with little or no human influence) the behavior of computer programs, hardware, and other technological artifacts. The intent is to discover bugs that have escaped during testing phases, or even to formally prove correctness properties of such programs.
Model checking (MC) is a formal verification technique that is loosely based on the exploration of state spaces of formal models of programs. It is considered the most successful FV technology in industry today and is heavily used in companies such as Intel, IBM, and Microsoft. The inventors of model checking, Edmund Clarke, Allen Emerson, and Joseph Sifakis, were recognized with the 2007 ACM Turing Award (see press release), considered the highest honor in computer science.

This course will cover the fundamentals of model checking. We will emphasize model checking of software, an area that has seen great advances over the past decade. Topics that will be covered include basic principles of model checking and temporal logic, automata-theoretic approaches, fixpoint theory, abstraction mechanisms and their practical implementation, symbolic reasoning using BDDs, SAT, and SMT, and concurrency and multi-threaded software verification.

This course is not about classical static analysis methods, such as control- or dataflow analyses, pointer analysis, etc. We will occasionally use these as tools, but we will not study them.

Goal and Methodology

The course is intended to provide Ph.D. or ambitious Master level students with a rigorous introduction to the field of formal verification in general and model checking in particular. If you are new in the program and are looking for a research topic, this course is for you. Bachelor students should (and Master students may want to) see Prerequisites below and then come and talk to me.

The course will be a combination of a series of lectures with a serious research component. In addition to studying fundamental and software-specific aspects of model checking, you will do homeworks, use and perhaps implement some software, read and evaluate (in the style of a scientific review) papers, and complete a research project.

Prerequisites

If you lack some of the prerequisites listed below, do not despair, but be prepared to catch up. If most of the below sound unfamiliar to you, you may not benefit much from this class.

Roughly in order of decreasing significance:
  • logic: thorough knowledge of propositional logic; basic knowledge of QBF and first-order predicate logic
  • graph theory: breadth and depth first search, strongly connected components, cycle detection
  • automata theory: finite-state automata over finite and infinite words; emptiness checks
  • static analysis techniques as used in compilers: alias and pointer analysis, pre- and postconditions
  • execution models of [asynchronous] concurrent software: thread interleavings; synchronization via locks, barriers, broadcast