Patrice Godefroid’s
Research Overview
February 2007
My main research area during
the last 18 years has been software model
checking in a broad sense. Here are some main themes. (I also worked on many
other smaller projects on other topics that cannot be summarized here -- please
see my list of publications for more information on those.)
Partial-Order Reduction
In 1988, I started doing
research under the supervision of Professor Pierre Wolper
on what is now known as partial-order
reduction. Partial-order reduction (POR) denotes a family of algorithmic
techniques for pruning the state spaces of concurrent reactive programs in such
a way that parts of the state space that are pruned away are guaranteed not to
contain error states of a specific type, such as deadlocks. POR can
considerably speed up verification by model checking, and is nowadays
implemented in many model checkers. With my advisor Pierre Wolper
and collaborators Gerard Holzmann and Didier Pirottin, we pioneered the development of POR, together
with other prominent contributors such as Doron Peled and Antti Valmari. My own work on POR culminated in January 1996 with
the publication of my PhD thesis in Springer's Lecture Notes in Computer Science series.
Software Model Checking via
Systematic Testing: VeriSoft
A year or so after joining Bell
Labs in 1994, I started working on software model checking, that is, how to
broaden the scope of model checking from abstract software systems (specified
in modeling languages) to concrete software systems (described using
programming languages). In 1996, I designed and implemented a first version of VeriSoft, the first model checker for analyzing software
written in mainstream programming languages such as C and C++. The main idea
behind of VeriSoft is simple: like a traditional
model checker computes the product of finite-state machines described in some
modeling language, VeriSoft computes the product of
operating-system (Unix-like) processes described in any programming language.
Several technical innovations made this possible: the use of a run-time
scheduler to systematically drive process executions, a construct to simulate nondeterminism at run-time, and the use of partial-order
reduction to make a search in the state space of concurrent OS processes
tractable even without storing any intermediate states in memory. Many of these
features have now been adopted in other software model checkers (like Java PathFinder, CMC, CHESS, etc.).
From 1996 to 2001, I worked
mostly on developing VeriSoft further. With several
Bell Labs colleagues, we investigated many extensions, described in several
published papers. We also started applying VeriSoft
to check the correctness of various software applications inside Lucent
Technologies. After several successful applications, VeriSoft
was also considered in 1999 for a Lucent-funded start-up. Working with Lucent's
venture-capitalist team was an enlightening experience. That same year, I
taught a course (mostly on VeriSoft) at
Software Model Checking via
Abstraction: May/Must Abstractions, 3-Valued Temporal Logics, and Generalized
Model Checking
Around 2000, another approach
to software model checking started to emerge: the static approach. Unlike VeriSoft, static software model checkers parse the source
code of the software to be checked, compute a conservative abstraction of the
original code, and then perform model checking on this abstraction. One of the
pioneering projects in that area is SLAM, a static software model checker for C
code, developed at Microsoft Research originally by Tom Ball and Sriram Rajamani. From 2001 to
2004, with Glenn Bruns, Radha
Jagadeesan and Michael Huth,
we developed a new framework for static software model checking that uses
may/must abstractions instead of may-only conservative abstractions. With such
abstractions, both proofs and counterexamples (bugs) are now guaranteed to be
sound, by construction. We also showed that verification results can sometimes
be more precise with generalized model
checking, which checks whether there exists a concretization of an
abstraction satisfying a temporal property. From a theoretical point of view,
generalized model checking is an interesting problem since it generalizes both
model checking (when the abstraction is complete) and satisfiability
(when the abstraction is completely unknown), probably the two most studied
problems related to temporal logic and verification. From a practical point of
view, our work in this area helps explain the foundation of static software
model checking.
Automating Software Testing
using Program Analysis: DART and SMART
In 2004, I started working with
renewed energy on how to extend the VeriSoft approach
(aka software model checking via systematic testing) to deal with data-driven
applications (after a first attempt described in a PLDI 1998 paper). With Nils Klarlund and Koushik Sen (both funded by my NSF grant with my Bell Labs
colleagues Dennis Dams and Kedar Namjoshi),
we implemented a first version of Directed
Automated Random Testing, or DART for short, a new approach to automate
testing that combines three main techniques: (1) automated interface extraction from source code, (2) random testing at that interface, and
(3) dynamic test generation to direct
executions along alternative program paths. The main strength of DART is that
testing can be performed completely automatically on any program that compiles,
as there is no need to manually write any test driver or harness code. Also,
whenever a symbolic expression cannot be generated for an expression involving
some input, the concrete value of that input can be used to simplify this
expression, which allows dynamic test generation to drive executions through
program statements that purely-static test generation cannot handle.
A DART directed search attempts
to sweep through all the feasible execution paths of a program using dynamic
test generation: the program under
test is first executed on some random or well-formed input, symbolic
constraints on inputs are gathered at conditional branches during that run, and
then a constraint solver is used to generate variants of the previous inputs in
order to steer the next execution of the program towards an alternative program
branch. This process is repeated until all (in
practice, many) feasible program paths of the program are executed, while
detecting various types of errors using run-time checking tools, like Purify,
for instance. DART can thus be viewed as one way of combining static (interface
extraction, symbolic execution) and dynamic (testing, run-time checking)
program analysis with model-checking techniques (systematic state-space
exploration).
Obviously, systematically
executing all feasible program paths does not scale to large, realistic
programs. In 2006, I developed a variant of the DART search algorithm that
performs dynamic test generation compositionally.
This new algorithm, dubbed SMART, eliminates path explosion due to interprocedural (interblock)
paths: the number of whole execution paths becomes linear in the number of intraprocedural paths, instead of being possibly
exponential. Moreover, for programs whose conditional statements can all be
driven using symbolic execution, this efficiency gain is obtained without
losing any precision. A SMART search is key to make
the DART approach (aka systematic dynamic test generation) scalable to large
programs.