Agenda

Verified Software Workshop and Summer School 2012

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

Rasmus Lerchedahl Petersen

10:30–10:45 Break

10:45–12:15

Theory Lecture 2

Tony Hoare | slides

Rasmus Lerchedahl Petersen | slides

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

Matthew Parkinson

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

Nikolaj Bjorner 

12:15–14:00    Lunch 
14:00–15:30  Hybrid Systems (1) 

Logical Analysis of Hybrid Systems: The KeYmaera Approach 1

André Platzer | slides

Jan-David Quesel 

15:30–15:45  Break 
15:45–17:15 

Logical Analysis of Hybrid Systems: The KeYmaera Approach 2

André Platzer and Jan-David Quesel

Thursday, August 30 
09:00–10:30  Hybrid Systems (II) 

Logical Analysis of Hybrid Systems: The KeYmaera Approach 3

André Platzer and Jan-David Quesel 

10:30–10:45  Break 
10:45–12:15 

Logical Analysis of Hybrid Systems: The KeYmaera Approach 4

André Platzer and Jan-David Quesel 

12:15–14:00    Lunch 
14:00–15:30  Tools (II) 

Software Model Checking 2 | slides

Patrice Godefroid

15:30–15:45  Break 
15:45–17:15 

Modern Satisfiability Modulo Theories Solvers in Program Analysis 2 | slides

Nikolaj Bjorner

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

Nikolaj Bjorner

12:15–14:00    Lunch 
14:00–15:30  Tools (IV) 

Software Model Checking 4 | slides

Patrice Godefroid  

15:30–15:45  Break 
15:45–17:15 

Modern Satisfiability Modulo Theories Solvers in Program Analysis 4 | slides

Nikolaj Bjorner

17:15–18:00    Wrap Up