09:15-10:30 Patrice Godefroid
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.
Title: From Dynamic Software Model Checking to Better Beer
Abstract: Dynamic software model checking consists of adapting model checking into a form of systematic testing that is applicable to industrial-size software. When I started research on this topic more than 20 years ago, I never imagined that it could one day help improve beer making. This talk will present this unexpected journey. Specifically (spoiler alert!), some key milestones are the birth of dynamic software model checking, DART, SAGE, how we deployed SAGE on a large scale inside Microsoft to find many security vulnerabilities, and how we recently launched the first commercial cloud fuzzing service, named Project Springfield.
In short, if you like model checking or beer, don’t miss this talk!
11:00-12:30 Session I
- Java Pathfinder on Android Devices, Alexander Kohan, Mitsuharu Yamamoto, Cyrille Artho, Yoriyuki Yamagata, Lei Ma, Masami Hagiya and Yoshinori Tanabe
- Towards Exhaustive Testing of Websites using JPF, Sarvesh Nagarajan, Nastaran Shafiei and Sarfraz Khurshid
- Resource Contracts for Java, Rody Kersten, Martin Schaef and Temesgen Kahsai
- Exploring Underdetermined Specifications using Java PathFinder, Alex Gyori, Ben Lambeth, Sarfraz Khurshid and Darko Marinov
14:00-15:30 Session II
- Symbolic Arrays in Symbolic PathFinder, Aymeric Fromherz, Kasper S. Luckow and Corina S. Pasareanu
- Staged Symbolic Execution for Parallel Property Checking, Junye Wen and Guowei Yang
- Releasing the PSYCO: Using symbolic search in interface generation for Java, Malte Mues, Falk Howar, Temesghen Kahsai, Kasper Luckow and Zvonimir Rakamaric
- StateComparator: Detecting unbounded variables using JPF, Heila Botha, Oksana Tkachuk, Brink Van Der Merwe and Willem Visser
16:00-16:30 Session III (short papers)
session chair: Kasper Luckow
- Visualization Support for JDart, Chaofeng Zhou, Falk Howar, Kasper Luckow and Zvonimir Rakamaric
- Monitoring Distributed Applications with Java Pathfinder, Lei Ma, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Alexander Kohan and Mitsuharu Yamamoto
16:30-17:50 JPF Open Discussion