Patrice Godefroid's Publications by Themes

Software Model Checking via Systematic Testing

HyperFuzzer: An Efficient Hybrid Fuzzer for Virtual CPUs (CCS'2021)
Intelligent REST API Data Fuzzing (ESEC/FSE'2020)
Differential Regression Testing for REST APIs (ISSTA'2020)
Checking Security Properties of Cloud Service REST APIs (ICST'2020)
Fuzzing: Hack, Art, and Science (CACM'2020)
RESTler: Stateful REST API Fuzzing (ICSE'2019)
Automated Software Test Generation: Some Challenges, Solutions, and Recent Advances (LNCS'10000)
Combining Model Checking and Testing (Handbook of Model Checking, 2018)
Deep Reinforcement Fuzzing (DLS'2018)
Learn&Fuzz: Machine Learning for Input Fuzzing (ASE'2017)
A General Framework for Dynamic Stub Injection (ICSE'2017)
Between Testing and Verification: Dynamic Software Model Checking (Marktoberdorf'2015)
IC-Cut: A Compositional Search Strategy for Dynamic Test Generation (SPIN'2015)
Proving Memory Safety of the ANI Windows Image Parser using Compositional Exhaustive Testing (VMCAI'2015)
Micro Execution (ICSE'2014)
Billions and Billions of Constraints: Whitebox Fuzz Testing in Production (ICSE'2013)
Test Generation Using Symbolic Execution (FSTTCS'2012)
From Program to Logic: An Introduction (LASER'2011)
Automated Synthesis of Symbolic Instruction Encodings from I/O Samples (PLDI'2012)
SAGE: Whitebox Fuzzing for Security Testing (ACM Queue and CACM'2012)
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation (SAS'2011)
Automatic Partial Loop Summarization in Dynamic Test Generation (ISSTA'2011)
Higher-Order Test Generation (PLDI'2011)
Symbolic Execution for Software Testing in Practice - Preliminary Assessment (ICSE'2011)
Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis (ISSTA'2010)
Compositional May-Must Program Analysis: Unleashing The Power of Alternation (POPL'2010)
Precise Pointer Reasoning for Dynamic Test Generation (ISSTA'2009)
Automating Software Testing Using Program Analysis (IEEE Software, 2008)
Active Property Checking (EMSOFT'2008)
Testing for Buffer Overflows with Length Abstraction (ISSTA'2008)
Grammar-based Whitebox Fuzzing (PLDI'2008)
Demand-Driven Compositional Symbolic Execution (TACAS'2008)
Automated Whitebox Fuzz Testing (NDSS'2008)
Compositional Dynamic Test Generation (POPL'2007)
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

May/Must Abstraction-Based Software Model Checking for Sound Verification and Falsification (Marktoberdorf'2013)
Analysis of Boolean Programs (TACAS'2013)
From Program to Logic: An Introduction (LASER'2011)
Compositional May-Must Program Analysis: Unleashing The Power of Alternation (POPL'2010)
LTL Generalized Model Checking Revisited (STTT'2011; journal version of VMCAI'2009)
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)

Recursive and Transactional State Machines

Analysis of Boolean Programs (TACAS'2013)
An Abort-Aware Model of Transactional Programming (STTT'2011; journal version of VMCAI'2009)
Analysis of Recursive State Machines (TOPLAS'2005; journal version of ICALP'2001)
Model Checking of Unrestricted Hierarchical State Machines (ICALP'2001)

Many-Valued Logics

Model Checking with Multi-Valued Logics (ICALP'2004)
Temporal Logic Query Checking (LICS'2001)

Specification Mining

Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs (TACAS'97)

Other Model-Checking Techniques

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)

Market Study

Concurrency at Microsoft - An Exploratory Survey (EC^2'2008)

Supply-Chain Security

What are Weak Links in the npm Supply Chain? (ICSE'2022)
Anomalicious: Automated Detection of Anomalous and Potentially Malicious Commits on GitHub (ICSE'2021)