Portrait of Patrice Godefroid

Patrice Godefroid

Partner Researcher


Patrice Godefroid is a Partner Researcher at Microsoft Research. He received a B.S. degree in Electrical Engineering (Computer Science elective) and a Ph.D. degree in Computer Science from the University of Liege, Belgium, in 1989 and 1994 respectively. From 1994 to 2006, he worked at AT&T/Lucent Bell Laboratories, where he was promoted to “distinguished member of technical staff” in 2001. His research interests include software model checking, program analysis, testing, verification, security and software engineering.

His main research topic during the last 25 years has been software model checking in a broad sense. Currently, he is 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. It is implemented in Microsoft tools like SAGE, PEX and YOGI.

Patrice is probably best known for his early work on partial-order reduction for model checking concurrent systems (his PhD thesis is published as LNCS volume 1032 by Springer), for his work on VeriSoft, the first software model checker for mainstream programming languages such as C and C++, for his work on 3-valued model checking with may/must abstractions for sound program verification and falsification, and for his work on automatic test generation with DART. More recently, he 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, he co-founded Project Springfield, the first commercial cloud fuzzing service, renamed Microsoft Security Risk Detection in May 2017.

Please visit his web-site for more information, including all his publications.