Verified Software Workshop 2009Part I: Lecture, October 17–18, 2009 | ||
| October 17, 2009 (Saturday) | ||
| Venue: B1 Auditorium, Microsoft Sigma Building | ||
| Morning | ||
| 09:00–09:10 | Welcome | |
| 09:10–10:40 |
Theory for Verified Software (Part I) Tony Hoare, 1980 Turing Award Winner, and Principal Researcher of Microsoft Research Cambridge | |
| 10:40–11:00 | Break and Group Photo | |
| 11:00–12:30 |
Software Analysis and Verification tools (Part I) Wolfram Schulte, Research Area Manager of Microsoft Research Redmond | |
| 12:30–13:30 | Lunch | |
| Afternoon | ||
| 13:30–15:00 |
International Initiative of Experiments for Verified Software (Part I) Jim Woodcock, Professor of Software Engineering, Department of Computer Science, University of York | |
| 15:00–15:20 | Break | |
| 15:20–16:20 |
Trustworthy Software in China Jifeng He, Member of Chinese Academy of Sciences, and Professor of East China Normal University | |
| 16:20–16:50 |
Research Update of Microsoft Research Asia Lintao Zhang, Researcher, Microsoft Research Asia | |
| 16:50–17:00 | Break | |
| 17:00–18:00 |
Panel discussion Moderator: Zheng Zhang, Principal Researcher, Research Area Manager, Microsoft Research Asia Panelists: Tony Hoare, Wolfram Schulte, Jim Woodcock, Jifeng He, Chaochen Zhou, Wei Li | |
| 18:00–20:00 | Welcome Banquet | |
| October 18, 2009 (Sunday) | ||
| Morning | ||
| 09:00–10:30 | Theory for Verified Software (Part II) Tony Hoare, 1980 Turing Award Winner, and Principal Researcher of Microsoft Research Cambridge | |
| 10:30–10:50 | Break | |
| 10:50–12:20 |
Software Analysis and Verification tools (Part II) Wolfram Schulte, Research Area Manager of Microsoft Research Redmond | |
| 12:20–13:30 | Lunch | |
| Afternoon | ||
| 13:30–15:00 | International Initiative of Experiments for Verified Software (Part II) Jim Woodcock, Professor of Software Engineering, Department of Computer Science, University of York | |
| 15:00–16:00 |
Research on verification in the Laboratory of Computer Science Huimin Lin, Member of Chinese Academy of Sciences, Director of the Laboratory for Computer Science, Institute of Software Chinese Academy of Sciences | |
|
16:00–16:20 |
Break | |
| 16:20–17:30 |
Panel discussion Moderator: Zheng Zhang Panelists: Tony Hoare, Wolfram Schulte, Jim Woodcock, Jifeng He, Chaochen Zhou, | |
| 17:30–20:00 |
Dinner | |
Part II: Presentation, October 19–20, 2009 | ||
| October 19, 2009 (Monday) | ||
| Venue: B1 Auditorium, Microsoft Sigma Building | ||
| Morning | ||
| 09:00–10:00 |
8,000 lines, one kernel, zero bugs Gernot Heiser, Professor, School of Computer Science and Engineering, | |
| 10:00–11:00 |
Automatically executing almost all statements with all values in real programs Dawson Engler, Associate Professor, Computer Science and Electrical Engineering, Stanford University | |
| 11:00–11:15 | Break | |
| 11:15-12:00 |
The FORMES Project Vania Joloboff and Jean-Pierre Jouannaud, LIAMA | |
| 12:00–13:30 | Lunch | |
| Afternoon | ||
| 13:30–14:30 |
Model Checking C++ Programs that use the STL Daniel Kroening, Professor, Computing Laboratory, University of Oxford | |
| 14:30–15:30 |
Generalizing Design-Space Exploration with FORMULA Ethan Jackson, Researcher, Microsoft Research Redmond | |
| 15:30–15:50 | Break | |
| 15:50–16:20 |
Static Analysis of Concurrent Programs for Bug Detection Dr. Cheng Zhang, Shanghai Jiaotong University | |
| 16:20–16:50 |
Data Mining Based Decomposition for Assume-Guarantee Reasoning Dr. Fei HE, Tsinghua University | |
| 16:50–17:20 |
Concurrent Dynamic Symbolic Execution Dr. Geguang PU, East China Normal University | |
|
17:20–17:50 |
Verification of pointer programs: An extension to Hoare logic Dr. Jianhua Zhao, Nanjing University | |
| 17:50–20:00 |
Dinner | |
|
October 20, 2009 (Tuesday) | ||
| 09:00–09:30 |
A decade of research in symbolic execution Dr. Jian Zhang, Institute of Software, Chinese Academy of Sciences | |
| 09:30–10:00 |
Software trustworthiness complexity analysis and trustworthiness measurement Dr. Wei WEI, Beihang University | |
| 10:00–10:30 |
Bounded Semantics of CTL and SAT-based Verification Dr. Wenhui Zhang, Institute of Software, Chinese Academy of Sciences | |
| 10:30–11:00 |
Abstraction of Object Graphs in Program Verification Dr. Yifeng Chen, Peking University | |
| 11:00–11:30 |
Our Researches on Verified Software: Compilation and Verification Dr. Yu Zhang, University of Science and Technology of China | |
| 11:30–12:30 |
Open discussion with cocktails at Sigma Building 5F lounge | |
- Workshop Home
- Agenda and Presentations
- Speakers
- Sponsors
- Image Gallery
