Patrice Godefroid

Email:	pg AT microsoft.com
Phone:	(425) 421-7938
Fax:	(425) 936-7329
Mail:	One Microsoft Way, Redmond, WA 98052, USA

Welcome to my new web-page! After 12 wonderful years at Bell Labs, I recently joined Microsoft Research (October 2006).

My main area of research is program specification, analysis, testing and verification.

My main research topic during the last 19 years has been software model checking in a broad sense. Currently, I am working mostly on automating software testing (and test generation in particular) using static and dynamic program analysis. This approach to software model checking via systematic testing combines program analysis, testing, model checking and theorem proving.

Here is a very brief bio and a recent research overview.

Some On-line Talks:

• 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.
• 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

• Upcoming: ASE'2008, FMICS'2008, TACAS'2009, ISSTA'2009
• Past: 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: (publicly available)

• VeriSoft is a tool for systematically testing concurrent reactive software written in any language (C, C++, etc.).
• Partial-Order Package for SPIN (Part of my PhD work done at the University of Liege; README file for this tool)

Some Publications: in reverse chronological order; see also my Publications by Themes

• 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) To appear in the Proceedings of EMSOFT'2008 (8th Annual ACM & IEEE International Conference on Embedded Software), ACM Press, Atlanta, October 2008.

• 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.

• LTL Generalized Model Checking Revisited (joint work with Nir Piterman) Microsoft Technical Report MSR-TR-2008-60, April 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.

• A Model of Transactional Programming (joint work with Kousha Etessami) Microsoft Technical Report MSR-TR-2008-19, January 2008.

• 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.

• 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.

• 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)