Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Agenda and Presentations

Verified Software Workshop 2009

Part 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

Download the presentation

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

Download the presentation – part 1

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

Download the presentation

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

Download the presentation

16:20–16:50

Research Update of Microsoft Research Asia

Lintao Zhang, Researcher, Microsoft Research Asia

Download the presentation

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

Download the presentation – part 2

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

Download the presentation

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,
Wei Li, Huimin Lin

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,
The University of New South Wales

Download the presentation

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

Download the presentation – part 1

Download the presentation – part 2

11:00–11:15 Break
11:15-12:00

The FORMES Project

Vania Joloboff and Jean-Pierre Jouannaud, LIAMA

Download the presentation – Joloboff

Download the presentation – Jouannaud

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

Download the presentation

14:30–15:30

Generalizing Design-Space Exploration with FORMULA

Ethan Jackson, Researcher, Microsoft Research Redmond

Download the presentation

15:30–15:50 Break
15:50–16:20

Static Analysis of Concurrent Programs for Bug Detection

Dr. Cheng Zhang, Shanghai Jiaotong University

Download the presentation

16:20–16:50

Data Mining Based Decomposition for Assume-Guarantee Reasoning

Dr. Fei HE, Tsinghua University

Download the presentation

16:50–17:20

Concurrent Dynamic Symbolic Execution

Dr. Geguang PU, East China Normal University

Download the presentation

17:20–17:50

Verification of pointer programs: An extension to Hoare logic

Dr. Jianhua Zhao, Nanjing University

Download the presentation

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

Download the presentation

10:00–10:30

Bounded Semantics of CTL and SAT-based Verification

Dr. Wenhui Zhang, Institute of Software, Chinese Academy of Sciences

Download the presentation

10:30–11:00

Abstraction of Object Graphs in Program Verification

Dr. Yifeng Chen, Peking University

Download the presentation

11:00–11:30

Our Researches on Verified Software: Compilation and Verification

Dr. Yu Zhang, University of Science and Technology of China

Download the presentation

11:30–12:30

Open discussion with cocktails at Sigma Building 5F lounge