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 VeriSoft is simple: like a traditional model checker computes the product of finite-state machines described in some modeling language, VeriSoft dynamically 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 Stanford University hosted by David Dill, another valuable experience (teaching a new course takes a lot of time!). Meanwhile, VeriSoft was gaining traction in some development and testing groups where its use contributed to finding several expensive, customer-visible bugs in various Lucent products. Since 1999, VeriSoft has also been publicly available outside Lucent and has been licensed to hundreds of users in industry and academia in more than 25 countries. In 2001, I was promoted to "distinguished member of the technical staff" of Bell Labs for essentially my work on VeriSoft and its successful applications in Lucent.

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.