Keynote Speakers
Title: Between Testing and Verification: Software Model Checking via Systematic Testing
Patrice Godefroid, Microsoft Research
Dynamic software model checking consists of adapting model checking into a form of systematic testing that is applicable to industrial-size software. Over the last two decades, dozens of tools following this paradigm have been developed for checking concurrent and data-driven software. Compared to traditional software testing, dynamic software model checking provides better coverage, but is more computationally expensive. Compared to more general forms of program verification like interactive theorem proving, this approach provides more limited verification guarantees, but is cheaper due to its higher level of automation. Dynamic software model checking thus offers an attractive practical trade-off between testing and formal verification.
This talk will review 20 years of research on dynamic software model checking. It will highlight some key milestones, applications, and successes. It will also discuss limitations, disappointments, and future work.
Speaker Bio
Patrice Godefroid is a Principal 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 Bell Laboratories (part of Lucent Technologies), where he was promoted to "distinguished member of technical staff" in 2001. His research interests include program (mostly software) specification, analysis, testing and verification.
Dr. Godefroid is probably best known for his pioneering 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.
Keynote Speakers
- Patrice Godefroid, Microsoft Research
- Stephen Bailey, Director of Emerging Technologies, Mentor Graphics
- Prof. Mooly Sagiv, Tel Aviv University
- Bodo Hoppe, Hardware Verification, IBM
