Synopsis


  • Course number: CS 7485
  • Class times: Mon & Wed, 2:50pm–4:30pm
  • Class location: Ryder Hall 435
  • Instructor: Thomas Wahl
  • Office hours: after each class meeting or by appointment, room 344, West Village H (my office)

Course topics


Formal verification (FV) refers to the concept of "mechanically" (i.e., based on a rigorous problem formalization, and more or less automatically) analyzing the behavior of programs, hardware, and other technological artifacts. The goal is to discover bugs (that have escaped during testing phases), or even to formally prove certain desirable 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 or hardware designs. 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 awarded the 2007 ACM Turing Award for their work (see ACM website).

The idea of exploring extensional program models, state by state, does not lend itself naturally to software, with very large, possibly nominally unbounded, state spaces. This hampered the application of model checking to programs in mainstream languages, until about 20 years ago, when two developments came together that would enable the break-through that the community had been waiting for: the insight that state spaces could be explored symbolically (rather than state by state), and the independent advances in automated reasoning procedures, such as satisfiability checkers for propositional and first-order logic formulas.

In this course we will learn about the foundations of model checking and the exciting field of temporal logics, which describe how truth changes over time. (The insight that programs should be analyzed using logics that reason over time was worth another Turing Award, in 1996, for Amir Pnueli.) We will then study techniques that specifically apply model checking to software, either domain-specific (such as communication protocol descriptions) or generic (for software written in system programming languages such as C). For details on the topics covered, see the Course description.

Intended audience and course format


The course is intended for Ph.D. and ambitious Master level students. If you are new in the CS program and are looking for a research topic, this course is for you. If you have come across the terms formal verification and model checking, including the praise and awards these techniques have amassed lately, and you want to know what all the fuzz is about, this course is for you. Most importantly, if you want to learn about techniques that you can use (now or in your professional future) to rid your programs of certain types of bugs that you suspect are still "in there", despite extensive testing, this course is again for you.

Since this topics course is not a follow-up to a core course that may have already laid the foundations, we have to earn those foundations. On the other hand, this makes this course fairly self-contained, suitable for anyone with basic knowledge in CS core material (see Prerequisites).

The course will start with a series of "lectures" that cover the core material. I put lectures in quotes because these will be informal, with discussion and question-and-answer components. The lectures will be accompanied by a few homeworks.

Interspersed throughout these initial lectures will be presentations by students of papers relevant for the current course material. Each presentation will be critiqued by the instructor and by your fellow students, in a suitable setting.

In the second part of the course, each student will work on a topic of choice in greater depth. This can take many forms; possibilities are listed in the Course description.

Prerequisites


If you lack some of the prerequisites listed below, just be prepared to catch up; we will help. If all of these sound completely unfamiliar to you, you may not benefit much from this class.

In order of decreasing significance:
  • logic: working knowledge of propositional logic; basic first-order predicate logic
  • graphs: breadth and depth first search, strongly connected components
  • finite-state automata: over finite and infinite words