Verified Software Workshop and Summer School 2012
- Home
- Agenda
- Speakers and Abstracts
On This Page
Verified Software Workshop Agenda
Thursday, August 23, 2012
|
Time |
Event/Topic | |
|
08:30–09:00 |
Guest Check-in | |
| 09:00–09:30 | Opening and Welcome | |
|
09:30–10:30 |
Algebra Unifies Theories of Programming | slides Tony Hoare, 1980 Turing Award Winner; principal researcher, Microsoft Research Cambridge | |
| 10:30–11:00 |
Break and Group Photo | |
| 11:00–12:00 |
A Clock-Based Framework For Modeling Hybrid Systems Jifeng He, Software Engineering Institute, East China Normal University, Member of Chinese Academy of Sciences | |
|
12:00–13:30 |
Lunch | |
|
13:30–14:30 |
Detecting Concurrency Bugs using Static and Dynamic Program Analyses | slides Aarti Gupta, department head, Systems Analysis and Verification, NEC Labs America | |
| 14:30–15:30 |
Safe Programming of Asynchronous Interaction: Can We Do It for Real? | slides Shaz Qadeer, senior researcher, Research in Software Engineering, Microsoft Research, Redmond | |
| 15:30–15:45 |
Break | |
| 15:45–16:45 |
Pervasive Model Checking Jin-Song Dong, National University of Singapore | |
| 16:45–17:30 | Panel Discussion | |
Friday, August 24, 2012
|
Time |
Event/Topic | |
|
09:00–10:00 |
Formal Analysis and Verification of Multiple Programs Based on Difference Identification | slides Masahiro Fujita, professor, University of Tokyo | |
| 10:00–11:00 |
Bounding and Sequentializing Concurrent Programs | slides Akash Lal, researcher, Microsoft Research India | |
|
11:00–11:20 |
Break | |
| 11:20–12:20 |
Verifying Concurrent Software | slides Daniel Kroening, professor of Computer Science, University of Oxford | |
| 12:20–14:00 | Lunch | |
|
14:00–15:00 |
Software Analytics and Its Application in Software Development Practice | slides Shi Han, associate researcher, Microsoft Research Asia | |
|
15:00–16:00 |
Modeling and Verification of Hybrid Systems | slides Chaochen Zhou, Institute of Software, Chinese Academy of Sciences. Member of Chinese Academy of Sciences | |
| 16:00–16:20 |
Break | |
| 16:20–17:10 |
Panel Discussion | |
| 17:10–17:30 | Wrap Up | |
| 18:00–20:00 | Welcome Dinner | |
Verified Software Summer School Agenda
August 27–31, 2012
|
Time |
Track |
Event/Topic | |
| Monday, August 27 | |||
|
09:00–10:30 |
Theory (I) |
Theory Lecture 1 Tony Hoare | slides 1 | slides 2 | slides 3 | |
| 10:30–10:45 | Break | ||
|
10:45–12:15 |
Theory Lecture 2 | ||
| 12:15–14:00 | Lunch | ||
| 14:00–15:30 | Experiments (I) |
Case Studies Using PAT | slides Sun Jun, Singapore University of Technology and Design | |
| 15:30–15:45 | Break | ||
| 15:45–17:15 |
SPARDL: A Modeling Framework for Periodic Control System Zheng Wang, China Academy of Space Technology | ||
| Tuesday, August 28 | |||
| 09:00–10:30 | Experiments (II) |
Spatio-Temporal UML Profile for Cyber-Physical Systems | slides Jing Liu, East China Normal University | |
| 10:30–10:45 | Break | ||
|
10:45–12:15 |
ORIENTAIS: A Formal Verified OSEK/VDX Real-Time Operating System Jianqi Shi, National University of Singapore | ||
|
12:15–14:00 |
Lunch | ||
| 14:00–16:00 | Theory (II) |
Separation Logic | slides | |
| 16:00–16:20 | Break | ||
| 16:20–16:50 | Theory Track Wrap Up | ||
| 19:30–21:00 |
Night of Theory for Verified Software Chaired by Tony Hoare | ||
| Wednesday, August 29 | |||
| 09:00–10:30 | Tools (I) | Software Model Checking 1 | slides Patrice Godefroid | |
| 10:30–10:45 | Break | ||
| 10:45–12:15 |
Modern Satisfiability Modulo Theories Solvers in Program Analysis 1 | slides | ||
| 12:15–14:00 | Lunch | ||
| 14:00–15:30 | Hybrid Systems (1) |
Logical Analysis of Hybrid Systems: The KeYmaera Approach 1 | |
| 15:30–15:45 | Break | ||
| 15:45–17:15 |
Logical Analysis of Hybrid Systems: The KeYmaera Approach 2 | ||
| Thursday, August 30 | |||
| 09:00–10:30 | Hybrid Systems (II) |
Logical Analysis of Hybrid Systems: The KeYmaera Approach 3 | |
| 10:30–10:45 | Break | ||
| 10:45–12:15 |
Logical Analysis of Hybrid Systems: The KeYmaera Approach 4 | ||
| 12:15–14:00 | Lunch | ||
| 14:00–15:30 | Tools (II) |
Software Model Checking 2 | slides | |
| 15:30–15:45 | Break | ||
| 15:45–17:15 |
Modern Satisfiability Modulo Theories Solvers in Program Analysis 2 | slides | ||
| Friday, August 31 | |||
| 09:00–10:30 | Tools (III) | Software Model Checking 3 | slides 1 | slides 2 Patrice Godefroid | |
| 10:30–10:45 | Break | ||
| 10:30–10:45 |
Modern Satisfiability Modulo Theories Solvers in Program Analysis 3 | slides | ||
| 12:15–14:00 | Lunch | ||
| 14:00–15:30 | Tools (IV) |
Software Model Checking 4 | slides | |
| 15:30–15:45 | Break | ||
| 15:45–17:15 |
Modern Satisfiability Modulo Theories Solvers in Program Analysis 4 | slides | ||
| 17:15–18:00 | Wrap Up | ||
