Verified Software: Theories, Tools, Experiments

Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to the latest Netscape.
More information

Conference Program
print page

Program Outline

All sessions take place in the Audimax, level F of the ETH main building (Hauptgebäude).

Monday, Oct. 10th, 2005

8:00-10:00: Registration
9:00-9:15 Welcome (Bertrand Meyer)
Chair: Jayadev Misra
9:15-9:45 Tony Hoare, Microsoft Research
Verified Software: Theories, Tools, Experiments
9:45-10:15 Keynote: Amir Pnueli, New York University, and Weizmann Institute of Science
Development of Reactive Systems: Property-Based vs. Model-Based
10:30-11:00: Coffee Break
Chair: Jim Woodcock
11:00-11:30Keynote: Wolfgang Paul, Universität Saarbrücken
Towards a Worldwide Verification Technology
11:30-11:45Steven Zdancewic, University of Pennsylvania
It is Time to Mechanize Programming Language Metatheory
11:45-12:00 Michael Ernst, Massachusetts Institute of Technology
Verification of Legacy Programs
12:00-12:15 Zhiming Liu, UNU-IIST Macao
Tools for Formal Software Engineering
12:30-12:45: Free time
12:45-14:00: Lunch
Chair: He Jifeng
14:00-14:30Keynote: Thomas Ball, Microsoft Research
The Verified Software Challenge: A call for a holistic approach to reliability
14:30-14:45Rajeev Joshi, NASA/JPL Laboratory for Reliable Software
A Mini Grand Challenge: Build a Verifiable Filesystem
14:45-15:00Cordell Green, Kestrel Institute
A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets
15:00-15:15Cliff Jones, Newcastle University
What can we do (technically) to get "the right specification"?
15:30-16:00: Coffee Break
16:00-17:00Panel: Challenge Codes
Bertrand Meyer, Willem Paul de Roever, Bernhard Steffen, Colin O'Halloran, Michael Butler
Moderator: Jim Woodcock
18:00-: Welcome Buffet

Tuesday, Oct. 11th, 2005

Chair: Ralph Back
9:00-9:30 Keynote: Anthony Hall, Oxford
Software Verification and Software Engineering: A Practitioner's Perspective
9:30-9:45 Colin O'Halloran, QinetiQ
Where is the value in a program verifier?
9:45-10:00 Kathi Fisler, Worcester Polytechnic University
Verification and Features
10:00-10:15 Jean-Raymond Abrial, ETH Zürich
Managing the Construction of Large Computerized Systems
10:30-11:00: Coffee Break
Chair: Masami Hagiya
11:00-11:30Keynote: Tom Reps, University of Wisconsin
Interprocedural analysis, and some remaining challenges
11:30-11:45Peter Müller, ETH Zürich
Reasoning about Object Structures Using Ownership
11:45-12:00David Naumann, Stevens Institute of Technology
Modular Reasoning in Object-Oriented Programming
12:00-12:15Peter O'Hearn, Queen Mary University of London
Scalable Specification and Reasoning: Challenges for Program Logic
12:30-12:45: Free time
12:45-14:00: Lunch
Chair: Panagiotis Manolios
14:00-14:30Keynote: Greg Nelson, HP SRC Classic, Palo Alto
Extended static checking
14:30-14:45Gary Leavens, Iowa State University
Lessons from the JML project
14:45-15:00Wolfram Schulte, Rustan Leino, Microsoft Research
The Spec# Programming System: Challenges and Directions
15:00-15:15Joseph Kiniry, University College Dublin
Integrating Static Checking and Interactive Verification
15:30-16:00: Coffee Break
16:00-17:00Panel: Methodologies
Moderator: Wolfram Schulte

Wednesday, Oct. 12th, 2005

Chair: Carolyn Talcott
9:00-9:30 Keynote: John Rushby, SRI International
Integrating Verification Components
9:30-9:45 Yves Bertot, INRIA
Dependent types, theorem proving, and applications for a verifying compiler
9:45-10:00 Bart Jacobs, Radboud University
Code-Carrying Theory
10:00-10:15 Douglas Smith, Kestrel Institute, Palo Alto
Generating Programs plus Proofs by Refinement
10:30-11:00: Coffee Break
Chair: Ganesan Ramalingam
11:00-11:30Keynote: Patrick Cousot, École normale supérieure, Paris
The Verification Grand Challenge and Abstract Interpretation
11:30-11:45Tom Reps, University of Wisconsin
Static Analysis of Executables
11:45-12:00Martin Rinard, Massachusetts Institute of Technology
Implications of a Data Structure Consistency Checking System
12:00-12:15Arnaud Venet, Kestrel Technology LLC
Towards a Homology Theory for Static Analysis
12:30-12:45: Free time
12:45-14:00: Lunch
Chair: Marsha Chechik
14:00-14:30Keynote: Gerard Holzmann, NASA/JPL Laboratory for Reliable Software
Reliable Software Systems Design
14:30-14:45Rajeev Alur, University of Pennsylvania
Trends and Challenges in Algorithmic Software Verification
14:45-15:00Helmut Veith, TU München
Model Checking: Back and Forth Between Hardware and Software
15:00-15:15Grigore Rosu, University of Illinois at Urbana-Champaign
Computational Logical Framework and Generic Program Analysis Technologies
15:30-16:00: Coffee Break
16:00-17:00Panel: Proof Tools
Tevfik Bultan, Daniel Kröning, Tiziana Margaria, Harald Ruess, Ofer Strichman, Aaron Stump
Moderator: Natarajan Shankar

Evening Program: Conference Dinner

Thursday, Oct. 13th, 2005

Chair: Constance Heitmeyer
9:00-9:30 Keynote: Mathai Joseph, Tata Consultancy Services
Formal Techniques in Large Scale Software Engineering
9:30-10:30 Panel: Dependability and Verification
Roderick Chapman, Cliff Jones, Mathai Joseph, John Rushby
Moderator: Constance Heitmeyer
10:30-11:00: Coffee Break
Chair: Jian Zhang, Chinese Academy of Sciences
11:00-11:30 Keynote: J Moore, University of Texas at Austin
A Mechanized Program Verifier
11:30-11:45 Jifeng He, UNU-IIST, Macao
Theories and Techniques of Program Modelling, Design and Verification
11:45-12:00 Kokichi Futatsugi, JAIST
Verifying Design with Proof Scores
12:00-12:15 Bertrand Meyer, ETH Zürich
Component = Contract + Implementation + Proof Obligation
12:30-12:45: Free time
12:45-14:00: Lunch
14:00-16:00Panel: Milestones and Road Map
Greg Nelson, Rajeev Joshi, Peter O'Hearn, Joseph Kiniry, J Moore, Natarajan Shankar
Moderator: Tony Hoare and Jayadev Misra