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