Patrice Godefroid's Publications by Themes

Software Model Checking via Systematic Testing

Software Partitioning for Effective Automated Unit Testing (EMSOFT'2006)
Software Model Checking: Searching for Computations in the Abstract or the Concrete (IFM'2005)
DART: Directed Automated Random Testing (PLDI'2005)
Dynamic Partial-Order Reduction for Model Checking Software (POPL'2005)
Software Model Checking: The VeriSoft Approach (FMSD'2005; journal version of POPL'97 paper)
Exploring Very Large State Spaces Using Genetic Algorithms (STTT'2004; journal version of TACAS'2002)
Software Model Checking in Practice: An Industrial Case Study (ICSE'2002)
VeriWeb: Automatically Testing Dynamic Web Sites (WWW'2002)
Ensuring Privacy in Presence Awareness Systems: An Automated Verification Approach (CSCW'2000)
Automated Systematic Testing for Constraint-Based Interactive Services (FSE'2000)
Exploiting Symmetry when Model-Checking Software (PSTV'99)
Design and Analysis of Communication Software (Stanford course, 1999)
Automatically Closing Open Reactive Programs (PLDI'98)
Systematic Software Testing using VeriSoft: An Analysis of the 4ESS Heart-Beat Monitor (BLTJ'98; journal version of ISSTA'98)
Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs (TACAS'97)
Model Checking for Programming Languages using VeriSoft (POPL'97) This paper describes VeriSoft, the first software model checker for mainstream programming languages such as C and C++.

Software Model Checking via Abstraction

Model Checking Vs. Generalized Model Checking: Semantic Minimizations for Temporal Logics (LICS'2005)
Three-Valued Abstractions of Games: Uncertainty, but with Precision (LICS'2004)
Reasoning about Abstract Open Systems with Generalized Module Checking (EMSOFT'2003)
On The Expressiveness of 3-Valued Models (VMCAI'2003)
Automatic Abstraction Using Generalized Model Checking (CAV'2002)
Abstraction-based Model Checking using Modal Transition Systems (CONCUR'2001)
Generalized Model Checking: Reasoning about Partial State Spaces (CONCUR'2000)
Model Checking Partial State Spaces with 3-Valued Temporal Logics (CAV'99)

Avoiding State Explosion in Model Checking (mostly thanks to Partial-Order Reduction)

Dynamic Partial-Order Reduction for Model Checking Software (POPL'2005)
Symmetry and Reduced Symmetry in Model Checking (TOPLAS'2004; journal version of CAV'2001)
On the Costs and Benefits of using Partial-Order Methods for the Verification of Concurrent Systems (Invited Paper) (POMIV'96)
Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs (TSE'96; journal version of ISSTA'96)
Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem (LNCS 1032, 1996; revised version of my PhD thesis)

My PhD thesis presents most of the results of my previous publications (before 1995) in a more comprehensive way. I highly recommend reading my thesis instead, preferably the LNCS revised version (my PhD thesis itself is available from here).

Symbolic Model Checking for Infinite State Systems

The Power of QDDs (SAS'97)
Symbolic Protocol Verification with Queue BDDs (LICS'96)
Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs (CAV'96)

Other Topics in Algorithmic Verification

Analysis of Recursive State Machines (TOPLAS'2005; journal version of ICALP'2001)
Model Checking with Multi-Valued Logics (ICALP'2004)
Model Checking of Unrestricted Hierarchical State Machines (ICALP'2001)
Temporal Logic Query Checking (LICS'2001)
Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs (TACAS'97)
State-Space Caching Revisited (FMSD'95; journal version of CAV'92)
On the Verification of Temporal Properties (PSTV'93)

Short Papers on Tools

VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software (CAV'97)
The ULg Partial-Order Package for SPIN (SPIN'95)

Applications of Model Checking (Case Studies)

Software Model Checking in Practice: An Industrial Case Study (ICSE'2002)
Systematic Software Testing using VeriSoft: An Analysis of the 4ESS Heart-Beat Monitor (BLTJ'98; journal version of ISSTA'98)
Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN (FME'96)