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