Patrice Godefroid
Contact: |
firstnamelastname AT hotmail.com
|
Warning: |
I will NOT reply to unsolicited requests, including journal review requests. |
Welcome to my web-page!
My area of expertise includes program
analysis, testing, verification, security, and software engineering.
Here is a very brief bio, a less brief bio, and a recent CV. This recent research overview summarizes most
of my work during the last 35+ years. My h-index
is growing faster than my age (but for how long?).
I am probably best known for my early work on partial-order
reduction for model checking concurrent systems (my PhD thesis is
published as LNCS volume 1032 by Springer), for my work on VeriSoft,
the first software model checker for mainstream programming languages
such as C and C++, for my work on 3-valued model checking with
may/must abstractions for sound program verification and
falsification, and for my work on automatic test generation with
DART. More recently, I co-developed SAGE, the first whitebox fuzzer
for security testing, which was credited to have found roughly one
third of all the security vulnerabilities discovered by file fuzzing
during the development of Microsoft's Windows 7. In 2015, I
co-founded Project Springfield, the first commercial cloud fuzzing
service. In 2017, I co-created RESTler, the first stateful
REST API fuzzing tool for automatically testing cloud services through
their APIs and finding security and reliability bugs in these services.
In 2022, I joined Lacework, a fast-growing cloud security startup,
to co-found its Code Security team; Lacework was acquired by Fortinet in 2024.
Research. My main research topic during the last 35+ years has been software model checking in a broad
sense. Specifically, my main broad research contribution has been the
development of dynamic
software model checking, a new approach to software model checking via systematic
testing that combines program analysis, testing, model checking,
and theorem proving. This approach is implemented in Microsoft tools
like SAGE, PEX, and
YOGI,
and in many other tools outside Microsoft.
After 12 years at Bell Labs, I joined Microsoft Research in 2006, and for
several years, my main project was SAGE, the first whitebox fuzzer
for security testing. SAGE extends systematic dynamic test generation
(introduced in DART) to
handle large applications and is optimized for long symbolic
executions at the x86 binary level. Since 2008, SAGE has found many new
expensive security bugs in many Windows applications. More information on the research
behind SAGE can be found in the papers below. See also SAGE in one
slide (old
version) and SAGE
for dummies (10min video). Our work on whitebox fuzzing and SAGE
(first published in 2008) was credited to introducing the "fuzzing"
problem to the program analysis, software engineering, and security
academic-research communities. SAGE also pioneered the use of search
heuristics based on code coverage for fuzzing purposes.
For a quick introduction to fuzzing, see Fuzzing: Hack, Art, and
Science (CACM'2020) and this (3min) video:
In 2015, I co-founded Project
Springfield and served as its CTO. Springfield is the first
commercial cloud fuzzing service. It was renamed Microsoft
Security Risk Detection in May 2017, and helped companies like OSIsoft
and Deschutes Brewery (video) and DocuSign
(video). It then evolved into an open-source fuzzing
platform called OneFuzz in 2020.
My next main project was RESTler, the first stateful
REST API fuzzer. Given a REST API specification of a cloud service,
RESTler automatically generates and executes tests that exercise the
service through its REST API, with the goal of finding security and
reliability bugs in the service. RESTler is now open-source on
GitHub (press
release).
In 2022, I joined Lacework to co-found its Code Security team. Our team
launched several new static-analysis products
for Software Composition Analysis
(i.e., identify all third-party vulnerable packages in code repos) and for finding security-related bugs in first-party code.
I also co-developed Code-Aware Agents (CAA), a new
runtime-monitoring tech to determine what code is executed (and not
executed) in the cloud, with very low cost so that this monitoring can run everywhere, all the time,
in production, and at cloud scale. CAA can detect whether vulnerable packages in
cloud workloads are ever being executed or not. And it turns out that most open-source packages
dragged into cloud workloads through dependencies are actually never executed anytime anywhere.
This is a game changer
for anyone who has ever had to prioritize what vulnerable packages to fix next.
Overall, our combined static and dynamic analyses extend the Lacework platform to cover the entire
development cycle of cloud services, from code to production.
Here is my
old Bell Labs web-page and my academic
genealogy.
Over the last 35+ years, I have been fortunate to work with
great collaborators, including the co-authors of the papers listed
below. I learned something from each of them and I thank them all.
Some On-line Talks:
- Vulnerability Management 2.0,
PNW-PLSE'2024 (video).
- Peter, the May and the Must, and Lacework,
O'HearnFest'2024 (video).
- Fuzzing @ Microsoft -
A Research Perspective, HCSS'2019 (Invited Talk; abstract).
- Dynamic Software Model
Checking for Security, Invited
Talk at EPFL, October 2018 (abstract; video).
- Automated Software
Testing for the 21st Century, TCE'2015 (Invited Talk; abstract; video).
- Dynamic Software Model
Checking, Ed Clarke Symposium 2014.
- 500 Machine-Years of
Software Model Checking and SMT Solving, SEFM'2014 (Invited Talk;
abstract ).
- Micro Execution,
ICSE'2014.
- Analysis of Boolean
Programs, TACAS'2013.
- Automated Synthesis of
Symbolic Instruction Encodings from I/O Samples, PLDI'2012.
- Tests from
Proofs, TAP'2011 & TOOLS'2011 (Invited talk; abstract ).
- Higher-Order Test
Generation, PLDI'2011.
- From Blackbox Fuzzing
to Whitebox Fuzzing towards Verification, ISSTA'2010 (Invited talk;
abstract ).
- Software Model
Checking Improving Security of a Billion Computers, SPIN'2009
(Invited talk;
abstract ).
- 20 Years of Research
on Software Model Checking, 2008 Médaille d'or du mérite
scientifique Gustave Trasenster de l'AILg (University of Liège
Alumni Award), March 2009.
- LTL Generalized
Model Checking Revisited, VMCAI'2009.
- An Abort-Aware
Model of Transactional Programming, VMCAI'2009.
- Automatic
Code-Driven Test Generation, SBMF'2008 (Invited talk).
- Software Model
Checking 2.0, Distinguished Lecture Series, Max Planck Institute
for Software Systems, April 2008 ( abstract ).
- Random Testing for Security: Blackbox vs. Whitebox Fuzzing, RT'2007 (Invited talk; abstract ).
- Compositional Dynamic Test
Generation, POPL'2007.
- Software Model
Checking via Static and Dynamic Program Analysis, MOVEP'2006
(Invited tutorial; abstract ; auxilliary file
slides.pdf to be included in slide 27).
- Software Model
Checking: Searching for Computations in the Abstract or the
Concrete, IFM'2005
(Invited talk; abstract
).
- Model Checking Vs.
Generalized Model Checking: Semantic Minimizations for Temporal
Logics, LICS'2005.
- Generalized Model
Checking, TIME'2005
(Invited talk;
abstract ).
- DART: Directed
Automated Random Testing, PLDI'2005.
- Model Checking with
Multi-Valued Logics, ICALP'2004.
- "Model Checking" Software
with VeriSoft, PASTE'2004 (Invited talk; abstract ).
- Model Checking of Software, SpecNCheck'2001 workshop (Invited talk; abstract ).
Some Professional Activities: Member of the program committee
for the conferences
- Past:
ICSE-SEIP'2022,
SAS'2021,
SPIN'2021,
VSTTE'2020,
PLDI'2020,
SPIN'2019,
CAV'2019,
SPIN'2018,
VSTTE'2018,
RV'2017,
SPIN'2017,
NFM'2017,
RV'2016,
PLDI'2016,
ICSE'2016 V2025,
CAV'2015,
PLDI'2015 (ERC),
TACAS'2015,
HVC'2014,
ATVA'2014,
ISSTA'2014,
TACAS'2014,
RV'2013,
SPIN'2013,
ICALP'2013,
FM'2012,
PLDI'2012,
TAP'2012,
TACAS'2012,
POPL'2012
(ERC), ATVA'2011, RV'2011, NFM'2011, SPIN'2010, ATVA'2010, RV'2010,TAP'2010, MoChArt'2010, MBT'2010, PLDI'2010 (ERC), VMCAI'2010, HVC'2009,
ISSTA'2009, TACAS'2009, FMICS'2008,
ASE'2008, LICS'2008,
TACAS'2008, RT'2007,
FMICS'2007, SPIN'2007,
CAV'2007, ISSTA'2007, VMCAI'2007, CAV'2006, LICS'2006,
VMCAI'2006, SPIN'2005
(PC chair), CAV'2005,
TACAS'2005,
ISSTA'2004, SPIN'2004, CONCUR'2003, TACAS'2003, ICSE'2003, SPIN'2003,
POPL'2002, TACAS'2002, FMICS'2002, CAV'2001, CAV'2000, FMSP'2000,
CAV'98, etc.
Some Software:
Some Publications: in reverse chronological order; see also my Publications by Themes
- What are Weak Links in the npm
Supply Chain? (joint work Nusrat Zahan, Tom Zimmermann, Brendan Murphy,
Chandra Maddila, and Laurie Williams) Proceedings of ICSE'2022
(International Conference on Software
Engineering), Software-Engineering-in-Practice Track,
Pittsburgh/virtual, May 2022.
- HyperFuzzer: An
Efficient Hybrid Fuzzer for Virtual CPUs (joint work with Xinyang
Ge, Ben Niu, Robert Brotzman, Yaohui Chen, HyungSeok Han, and Weidong
Cui) Proceedings of CCS'2021 (ACM Conference on Computer and
Communications Security), November 2021.
- Anomalicious: Automated
Detection of Anomalous and Potentially Malicious Commits on GitHub
(joint work with Danielle Gonzalez, Tom Zimmermann, and Max Schafer)
Proceedings of ICSE'2021 (International Conference on Software
Engineering), Software-Engineering-in-Practice Track,
Madrid/virtual, May 2021.
- Intelligent REST API Data
Fuzzing (joint work with Bo-Yuan Huang and Marina Polishchuk)
Proceedings of ESEC/FSE'2020 (ACM Joint European Software Engineering
Conference and Symposium on the Foundations of Software Engineering),
Sacramento/virtual, November 2020.
- Differential Regression
Testing for REST APIs (joint work with Daniel Lehmann and Marina
Polishchuk) Proceedings of ISSTA'2020 (International Symposium on
Software Testing and Analysis), Los Angeles/virtual, July 2020.
- Checking Security
Properties of Cloud Service REST APIs (joint work with Vaggelis
Atlidakis and Marina Polishchuk) Proceedings of ICST'2020 (IEEE
International Conference on Software Testing, Verification and
Validation), Porto, March 2020.
- Fuzzing: Hack,
Art, and Science Communications of the ACM, Volume 63, Number 2,
pages 70-76, February 2020. Links to CACM
on-line article and video.
- Root Causing Flaky Tests
in a Large-scale Industrial Setting (joint work with Wing Lam,
Suman Nath, Anirudh Santhiar and Suresh Thummalapenta) Proceedings of
ISSTA'2019 (International Symposium on Software Testing and Analysis),
pages 101-111, Beijing, July 2019.
- RESTler: Stateful REST API
Fuzzing (joint work with Vaggelis Atlidakis and Marina
Polishchuk) Proceedings of ICSE'2019 (41st International Conference on
Software Engineering), pages 748-758, Montreal, May 2019. (Earlier
version in
MSR-TR-2018-11 , April 2018.)
- Automated Software
Test Generation: Some Challenges, Solutions, and Recent Advances
(joint work with George Candea) Special
Issue LNCS 10000 (Computing and Software Science: State of the Art
and Perspectives), Lecture Notes in Computer Science, vol. 10000,
pages 505-531, Springer, 2018.
- Combining Model
Checking and Testing (joint work with Koushik Sen) Chapter 19 of
the Handbook
of Model Checking , pages 613-649, Springer, 2018.
- Deep Reinforcement Fuzzing
(joint work with Konstantin Bottinger and Rishabh Singh)
Proceedings of DLS'2018 (1st Deep Learning and Security Workshop), San
Francisco, May 2018.
- Learn&Fuzz: Machine
Learning for Input Fuzzing (joint work with Hila Peleg and
Rishabh Singh) Proceedings of ASE'2017 (32nd
International Conference on Automated Software Engineering), pages 50-59,
Urbana-Champaign, October 2017.
- A General Framework for
Dynamic Stub Injection (joint work with Maria Christakis, Patrick
Emmisberger, and Peter Muller) Proceedings of
ICSE'2017 (39th International Conference on Software Engineering), pages
586-596, Buenos Aires, May 2017.
- Between Testing
and Verification: Dynamic Software Model Checking Proceedings of
Marktoberdorf'2015 (Dependable Software Systems Engineering, NATO
Science for Peace and Security Series, IOS Press 2016), pages 99-116,
Marktoberdorf, August 2015.
- IC-Cut: A Compositional
Search Strategy for Dynamic Test Generation (joint work with
Maria Christakis) Proceedings of SPIN'2015 (22nd International SPIN
Symposium on Model Checking of Software), Stellenbosch, August
2015. Lecture Notes in Computer Science, vol. 9232, pages 300-318,
Springer-Verlag.
- Checking Beliefs in
Dynamic Networks (joint work with Nuno Lopes, Nikolaj Bjorner,
Karthick Jayaraman, and George Varghese) Proceedings of NSDI'2015
(12th USENIX Symposium on Networked Systems Design and
Implementation), Oakland, May 2015.
- Proving Memory Safety of
the ANI Windows Image Parser using Compositional Exhaustive Testing
(joint work with Maria Christakis) Proceedings of VMCAI'2015
(16th International Conference on Verification, Model Checking, and
Abstract Interpretation), Mumbai, January 2015. Lecture Notes in
Computer Science, vol. 8931, pages 370-389, Springer-Verlag.
- Micro Execution
Proceedings of ICSE'2014 (International Conference on Software
Engineering), pages 539-549, Hyderabad, June 2014.
- May/Must
Abstraction-Based Software Model Checking for Sound Verification and
Falsification Proceedings of Marktoberdorf'2013 (NATO Advanced
Study Institute on Software Systems Safety), pages 1-16,
Marktoberdorf, August 2013.
- Billions and Billions of
Constraints: Whitebox Fuzz Testing in Production (joint work with
Ella Bounimova and David Molnar) Proceedings of ICSE'2013
(International Conference on Software Engineering), pages 122-131, San
Francisco, May 2013.
- Analysis of Boolean
Programs (joint work with Mihalis Yannakakis) Proceedings of
TACAS'2013 (Tools and Algorithms for the Construction and Analysis of
Systems), Rome, March 2013. Lecture Notes in Computer Science,
vol. 7795, pages 214-229, Springer-Verlag. (Full version with
proofs)
- Test Generation Using
Symbolic Execution (Invited paper) Proceedings of FSTTCS'2012
(IARCS Annual Conference on Foundations of Software Technology and
Theoretical Computer Science), pages 24-33, Hyderabad, December
2012.
- From Program to Logic: An
Introduction (joint work with Shuvendu K. Lahiri) Proceedings of
LASER'2011 (LASER'2011 Summer School), December 2012. Lecture Notes in
Computer Science, vol. 7682, pages 31-44, Springer-Verlag.
- Automated Synthesis of
Symbolic Instruction Encodings from I/O Samples (joint work with
Ankur Taly) Proceedings of PLDI'2012 (33rd ACM SIGPLAN conference on
Programming Language Design and Implementation), pages 441-452,
Beijing, June 2012.
- SAGE: Whitebox Fuzzing for
Security Testing (joint work with Michael Y. Levin and David
Molnar) Communications of the ACM, Volume 55, Number 3, pages 40-44,
March 2012.
On-line version in ACM Queue 10(1):20, January 2012.
- An
Abort-Aware Model of Transactional Programming (joint work with
Kousha Etessami) Software Tools for Technology Transfer,
13(6):537-551, September 2011. (Journal version of VMCAI'2009
paper.)
- LTL Generalized Model
Checking Revisited (joint work with Nir Piterman) Software Tools
for Technology Transfer, 13(6):571-584, September 2011. (Journal
version of VMCAI'2009 paper.)
- Statically Validating Must
Summaries for Incremental Compositional Dynamic Test Generation
(joint work with Shuvendu K. Lahiri and Cindy Rubio-Gonzalez)
Proceedings of SAS'2011 (18th International Static Analysis
Symposium), Venice, September 2011. Lecture Notes in Computer Science,
vol. 6887, pages 112-128, Springer-Verlag. (A preliminary version
titled
"Incremental Compositional Dynamic Test Generation" appeared as
MSR Technical Report MSR-TR-2010-11, February 2010.)
- Automatic Partial Loop
Summarization in Dynamic Test Generation (joint work with Daniel
Luchaup) Proceedings of ISSTA'2011 (International Symposium on
Software Testing and Analysis), pages 23-33, Toronto, July
2011. (Distinguished paper award)
- Higher-Order Test
Generation Proceedings of PLDI'2011 (32nd ACM SIGPLAN conference
on Programming Language Design and Implementation), pages 258-269, San
Jose, June 2011.
- Symbolic Execution for
Software Testing in Practice - Preliminary Assessment (joint work
with Cristian Cadar, Sarfraz Khurshid, Corina Pasareanu, Koushik Sen,
Nikolai Tillmann and Willem Visser) Proceedings of ICSE'2011
(International Conference on Software Engineering), Impact Track,
pages 1066-1071, Honolulu, May 2011.
- Proving Memory Safety of
Floating-Point Computations by Combining Static and Dynamic Program
Analysis (joint work with Johannes Kinder) Proceedings of
ISSTA'2010 (International Symposium on Software Testing and Analysis),
pages 1-11, Trento, July 2010.
-
Fuzzing in The Cloud (Position Statement) (joint work with David
Molnar) MSR Technical Report MSR-TR-2010-29, March 2010.
- Compositional May-Must
Program Analysis: Unleashing The Power of Alternation (joint work
with Aditya Nori, Sriram Rajamani and Sai Deep Tetali) Proceedings of
POPL'2010 (37th Annual ACM Symposium on Principles of Programming
Languages), pages 43-55, Madrid, January 2010.
- Precise Pointer Reasoning
for Dynamic Test Generation (joint work with Bassem Elkarablieh
and Michael Y. Levin) Proceedings of ISSTA'2009 (International
Symposium on Software Testing and Analysis), pages 129-139, Chicago,
July 2009.
- LTL Generalized
Model Checking Revisited (joint work with Nir Piterman)
Proceedings of VMCAI'2009 (10th Conference on Verification, Model
Checking and Abstract Interpretation), Savannah, January 2009. Lecture
Notes in Computer Science, vol. 5403, pages 89-104,
Springer-Verlag.
- An Abort-Aware
Model of Transactional Programming (joint work with Kousha
Etessami) Proceedings of VMCAI'2009 (10th Conference on Verification,
Model Checking and Abstract Interpretation), Savannah, January
2009. Lecture Notes in Computer Science, vol. 5403, pages 59-73,
Springer-Verlag. (Full version as MSR
Technical Report MSR-TR-2008-159.)
- Automating Software
Testing Using Program Analysis (joint work with Peli de Halleux,
Michael Y. Levin, Aditya V. Nori, Sriram K. Rajamani, Wolfram Schulte
and Nikolai Tillmann) IEEE Software, Volume 25, Number 5, pages 30-37,
September/October 2008.
- Active Property
Checking (joint work with Michael Y. Levin and David Molnar)
Proceedings of EMSOFT'2008 (8th Annual ACM & IEEE International
Conference on Embedded Software), ACM Press, pages 207-216, Atlanta,
October 2008. (Extended version with "active type checking" as MSR
Technical Report MSR-TR-2007-91.)
- Testing for Buffer
Overflows with Length Abstraction (joint work with Ru-Gang Xu and
Rupak Majumdar) Proceedings of ISSTA'2008 (International Symposium on
Software Testing and Analysis), pages 27-38, Seattle, July 2008.
- Concurrency at Microsoft - An
Exploratory Survey (joint work with Nachi Nagappan) Proceedings of
(EC)^2 (CAV 2008 Workshop on "Exploiting Concurrency Efficiently and
Correctly"), Princeton, July 2008.
- Grammar-based Whitebox
Fuzzing (joint work with Adam Kiezun and Michael Y. Levin)
Proceedings of PLDI'2008 (ACM SIGPLAN 2008 Conference on Programming
Language Design and Implementation), pages 206-215, Tucson, June
2008.
- Demand-Driven
Compositional Symbolic Execution (joint work with Saswat Anand and
Nikolai Tillmann) Proceedings of TACAS'2008 (Tools
and Algorithms for the Construction and Analysis of Systems),
Budapest, April 2008. Lecture Notes in Computer
Science, vol. 4963, pages 367-381, Springer-Verlag.
- Automated Whitebox Fuzz
Testing (joint work with Michael Y. Levin and David Molnar)
Proceedings of NDSS'2008 (Network and Distributed Systems Security),
pages 151-166, San Diego, February 2008. (NDSS 2022 Test-of-Time Award)
- Compositional Dynamic Test
Generation Proceedings of POPL'2007 (34th Annual ACM Symposium on
Principles of Programming Languages), pages 47-54, Nice, January 2007.
- Software Partitioning
for Effective Automated Unit Testing (joint work with Arindam
Chakrabarti) Proceedings of EMSOFT'2006 (6th Annual ACM & IEEE
International Conference on Embedded Software), ACM Press, pages
262-171, Seoul, October 2006.
- Software Model
Checking: Searching for Computations in the Abstract or the
Concrete (joint work with Nils Klarlund) Invited paper.
Proceedings of IFM'2005 (Fifth International Conference on Integrated
Formal Methods), Eindhoven, November 2005. Lecture Notes in Computer
Science, vol. 3771, pages 20-32, Springer-Verlag. (Older IFM'2005
proceedings version written
in August 2005.)
- Analysis of Recursive
State Machines (joint work with Rajeev Alur, Michael Benedikt,
Kousha Etessami, Thomas Reps and Mihalis Yannakakis) ACM Transactions
on Programming Languages and Systems (TOPLAS), Volume 27, Number 4,
pages 786-818, July 2005, ACM Press. (Journal version of ICALP'2001
paper.)
- The Soundness of Bugs is
What Matters (Position Statement) Proceedings of BUGS'2005
(PLDI'2005 Workshop on the Evaluation of Software Defect Detection
Tools), Chicago, June 2005.
- DART: Directed Automated
Random Testing (joint work with Nils Klarlund and Koushik Sen)
Proceedings of PLDI'2005 (ACM SIGPLAN 2005 Conference on Programming
Language Design and Implementation), pages 213-223, Chicago, June
2005. (HVC'2009
award for "the most promising contribution to fields of software
and hardware verification and test in the last five years")
- Model Checking Vs.
Generalized Model Checking: Semantic Minimizations for Temporal Logics
(joint work with Michael Huth) Proceedings of LICS'2005 (20th
IEEE Symposium on Logic in Computer Science), pages 158-167, Chicago,
June 2005.
- Software Model Checking: The
VeriSoft Approach Formal Methods in System Design, Kluwer Academic
Publishers, volume 26, number 2, pages 77-101, March 2005. Also
available as Bell Labs Technical Memorandum ITD-03-44189G, March
2003.
- Dynamic Partial-Order
Reduction for Model Checking Software (joint work with Cormac
Flanagan) Proceedings of POPL'2005 (32nd ACM Symposium on Principles
of Programming Languages), pages 110-121, Long Beach, January
2005. (Addendum)
- Exploring Very Large
State Spaces Using Genetic Algorithms (joint work with Sarfraz
Khurshid) International Journal on Software Tools for Technology
Transfer (STTT), Volume 6, Number 2, pages 117-127, August 2004,
Springer-Verlag. (Journal version of TACAS'2002 paper.)
- Symmetry and Reduced
Symmetry in Model Checking (joint work with Prasad Sistla) ACM
Transactions on Programming Languages and Systems (TOPLAS), Volume 26,
Number 4, pages 702-734, July 2004, ACM Press. (Journal version of
CAV'2001 paper.)
- Three-Valued Abstractions
of Games: Uncertainty, but with Precision (joint work with Luca de
Alfaro and Radha Jagadeesan) Proceedings of LICS'2004
(19th IEEE Symposium on Logic in Computer Science), pages 170-179, Turku,
July 2004.
- Model Checking with
Multi-Valued Logics (joint work with Glenn Bruns) Proceedings of
ICALP'2004 (31st International Colloquium on Automata, Languages and
Programming), Turku, July 2004. Lecture Notes in Computer Science,
vol. 3142, pages 281-293, Springer-Verlag. (Previous version in Bell Labs
Technical Memorandum
ITD-03-44535H, May 2003.)
- Reasoning about Abstract
Open Systems with Generalized Module Checking Proceedings of
EMSOFT'2003 (3rd ACM & IEEE International Conference on Embedded
Software), Philadelphia, October 2003. Lecture Notes in Computer
Science, vol. 2855, pages 223-240, Springer-Verlag.
- On The Expressiveness of
3-Valued Models (joint work with Radha Jagadeesan) Proceedings of
VMCAI'2003 (4th Conference on Verification, Model Checking and
Abstract Interpretation), New York, January 2003. Lecture Notes in
Computer Science, vol. 2575, pages 206-222, Springer-Verlag.
- Automatic Abstraction Using
Generalized Model Checking (joint work with Radha Jagadeesan)
Proceedings of CAV'2002 (14th Conference on Computer Aided
Verification), Copenhagen, July 2002. Lecture Notes in Computer
Science, vol. 2404, pages 137-150, Springer-Verlag.
- VeriWeb: Automatically
Testing Dynamic Web Sites (joint work with Michael Benedikt and
Juliana Freire) Proceedings of WWW'2002 (11th International World Wide
Web Conference), Honolulu, May 2002.
- Software Model Checking in
Practice: An Industrial Case Study (joint work with Satish Chandra
and Chris Palm) Proceedings of ICSE'2002 (International Conference on
Software Engineering), pages 431-441, Orlando, May 2002.
- Exploring Very Large State
Spaces Using Genetic Algorithms (joint work with Sarfraz Khurshid)
Proceedings of TACAS'2002 (Tools and Algorithms for the Construction
and Analysis of Systems), Grenoble, April 2002.
- Abstraction-based Model
Checking using Modal Transition Systems (joint work with Michael
Huth and Radha Jagadeesan) Proceedings of CONCUR'2001 (12th
International Conference on Concurrency Theory), Aalborg, August
2001. Lecture Notes in Computer Science, vol. 2154, pages 426-440,
Springer-Verlag.
- Symmetry and Reduced
Symmetry in Model Checking (joint work with Prasad Sistla)
Proceedings of CAV'2001 (13th Conference on Computer Aided
Verification), Paris, July 2001. Lecture Notes in Computer Science,
vol. 2102, pages 91-103, Springer-Verlag.
- Model Checking of
Unrestricted Hierarchical State Machines (joint work with Michael
Benedikt and Tom Reps) Proceedings of ICALP'2001 (28th International
Colloquium on Automata, Languages and Programming), Crete, Greece,
July 2001. Lecture Notes in Computer Science, vol. 2076, pages
652-666, Springer-Verlag.
- Temporal Logic Query
Checking (joint work with Glenn Bruns) Proceedings of LICS'2001
(16th IEEE Symposium on Logic in Computer Science), pages 409-417,
Boston, June 2001.
- Ensuring Privacy in
Presence Awareness Systems: An Automated Verification Approach
(joint work with Jim Herbsleb, Lalita Jagadeesan, and Du Li)
Proceedings of CSCW'2000 (ACM 2000 Conference on Computer Supported
Cooperative Work), Philadelphia, December 2000.
- Automated Systematic Testing
for Constraint-Based Interactive Services (joint work with Lalita
Jagadeesan, Radha Jagadeesan and Konstantin Laufer) Proceedings of
FSE'2000 (8th International Symposium on the Foundations of Software
Engineering), pages 40-49, San Diego, November 2000.
- Generalized Model
Checking: Reasoning about Partial State Spaces (joint work with
Glenn Bruns) Proceedings of CONCUR'2000 (11th International Conference
on Concurrency Theory), University Park, August 2000. Lecture Notes in
Computer Science, vol. 1877, pages 168-182, Springer-Verlag.
- In the fall of 1999, I have given a course entitled Design and Analysis of Communication
Software at Stanford University, in collaboration with David
L. Dill.
- Exploiting Symmetry when
Model-Checking Software Proceedings of FORTE/PSTV'99 (Formal
Methods for Protocol Engineering and Distributed Systems), pages
257-275, Beijing, October 1999.
- Model Checking Partial State Spaces
with 3-Valued Temporal Logics (joint work with Glenn Bruns)
Proceedings of CAV'99 (11th Conference on Computer Aided Verification),
Trento, July 1999. Lecture Notes in Computer Science, vol. 1633, pages
274-287, Springer-Verlag.
- Automatically Closing Open Reactive
Programs (joint work with Christopher Colby and Lalita Jagadeesan)
Proceedings of PLDI'98 (1998 ACM SIGPLAN Conference on Programming Language
Design and Implementation), pages 345-357, Montreal, June 1998.
- Systematic Software Testing using
VeriSoft: An Analysis of the 4ESS Heart-Beat Monitor (joint work
with Bob Hanmer and Lalita Jagadeesan) Bell Labs Technical Journal,
Volume 3, Number 2, April-June 1998.
- Model Checking Without a Model:
An Analysis of the Heart-Beat Monitor of a Telephone Switch using
VeriSoft (joint work with Bob Hanmer and Lalita Jagadeesan)
Proceedings of ISSTA'98 (1998 ACM SIGSOFT International Symposium on
Software Testing and Analysis), pages 124-133, Clearwater Beach, March
1998.
- The Power of QDDs (joint
work with Bernard Boigelot, Bernard Willems and Pierre Wolper)
Proceedings of SAS'97 (Fourth International Static Analysis Symposium),
Paris, September 1997. Lecture Notes in Computer Science, vol. 1302,
pages 172-186, Springer-Verlag.
- VeriSoft: A Tool for the Automatic
Analysis of Concurrent Reactive Software (short paper) Proceedings
of CAV'97 (9th Conference on Computer Aided Verification), Haifa, June
1997. Lecture Notes in Computer Science, vol. 1254, pages 476-479,
Springer-Verlag.
- Automatic Synthesis of
Specifications from the Dynamic Observation of Reactive Programs
(joint work with Bernard Boigelot) Proceedings of TACAS'97 (Third
International Workshop on Tools and Algorithms for the Construction
and Analysis of Systems), Twente, April 1997. Lecture Notes in
Computer Science, vol. 1217, pages 321-333, Springer-Verlag.
- Model Checking for
Programming Languages using VeriSoft Proceedings of POPL'97 (24th ACM
Symposium on Principles of Programming Languages), pages 174-186,
Paris, January 1997.
- On the Costs and Benefits of
using Partial-Order Methods for the Verification of Concurrent Systems
(Invited Paper) Proceedings of DIMACS Workshop on Partial-Order
Methods in Verification, AMS, Princeton, July 1996.
- Symbolic Protocol
Verification with Queue BDDs (joint work with David Long)
Formal Methods in System Design, Kluwer Academic Publishers, volume
14, number 3, pages 257-271, May 1999. Preliminary version in
Proceedings of LICS'96 (11th IEEE Symposium on Logic in Computer Science),
pages 198-206, New Brunswick, July 1996.
- Symbolic Verification of
Communication Protocols with Infinite State Spaces using QDDs
(joint work with Bernard Boigelot) Formal Methods in System Design,
Kluwer Academic Publishers, volume 14, number 3, pages 237-255, May
1999. Preliminary version in Proceedings of CAV'96 (8th Conference on
Computer Aided Verification), New Brunswick, August 1996. Lecture
Notes in Computer Science, vol. 1102, pages 1-12, Springer-Verlag.
- Using Partial-Order
Methods in the Formal Validation of Industrial Concurrent Programs
(joint work with Doron Peled and Mark Staskauskas) IEEE
Transactions on Software Engineering, volume 22, number 7, pages
496-507, July 1996. Preliminary version in Proceedings of ISSTA'96
(1996 ACM SIGSOFT International Symposium on Software Testing and
Analysis), pages 261-269, San Diego, January 1996.
- Model Checking in
Practice: An Analysis of the ACCESS.bus Protocol using SPIN
(joint work with Bernard Boigelot) Proceedings of FME'96 (Formal
Methods Europe'96), Oxford, March 1996. Lecture Notes in Computer
Science, vol. 1051, pages 465-478, Springer-Verlag.
- A revised version of my PhD thesis, "Partial-Order Methods for
the Verification of Concurrent Systems -- An Approach to the
State-Explosion Problem", is published by Springer-Verlag, as volume 1032
of Lecture Notes in Computer Science, January 1996. (ISBN
3-540-60761-7)
- The ULg
Partial-Order Package for SPIN (short paper) Presented at the
first SPIN workshop, Montreal, October 1995. This short document
presents an overview of the Partial-Order Package for SPIN developed
at the University of Liege (ULg) in 1992 -- 1994, by Didier Pirottin
and me, under the supervision of Pierre Wolper, and with the
collaboration of Gerard Holzmann.
- State-Space Caching
Revisited (joint work with Gerard Holzmann and Didier Pirottin)
Formal Methods in System Design, Kluwer Academic Publishers, volume 7,
number 3, pages 1-15, November 1995. (Journal version of CAV'92
paper.)
- On the Verification of
Temporal Properties (joint work with Gerard Holzmann) Proceedings
of PSTV'93 (13th IFIP WG 6.1 International Symposium on Protocol
Specification, Testing, and Verification), pages 109-124, Liege, May
1993. North-Holland.
Previous Publications (1990-1994)
Copyright Notice: The above material is
presented to ensure timely dissemination of scholarly and technical
work. Copyright and all rights therein are retained by authors or by
other copyright holders. All persons copying this information are
expected to adhere to the terms and constraints invoked by each
author's copyright. In most cases, these works may not be reposted
without the explicit permission of the copyright holder.
Some Words of Wisdom (Quotes)
- Never make small plans. (Burnham)
- Where there is a will, there is a way. (Mom?)
- Just do it. (Nike?)
- Imagination is more important than knowledge. (Albert Einstein)
- Imitation is the most sincere form of flattery. (Unknown)
- Don't worry about things you have no control over. (Unknown)
- Be the change you want to see in the world. (Mahatma Gandhi)
- Change your thoughts and you change your world. (Norman Vincent Peale)
- Life is hard. Science is harder. (Anne-Christine Poncelet)