 |
|
||||||||||
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
Program Outline
All sessions take place in the Audimax, level F of the ETH main building (Hauptgebäude).
Monday, Oct. 10th, 2005
| Time | Talk/Event |
|---|---|
| 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:15-10:30 | Summary/Discussion |
| 10:30-11:00: Coffee Break | |
| Chair: Jim Woodcock | |
| 11:00-11:30 | Keynote: Wolfgang Paul, Universität Saarbrücken Towards a Worldwide Verification Technology |
| 11:30-11:45 | Steven 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:15-12:30 | Summary/Discussion |
| 12:30-12:45: Free time | |
| 12:45-14:00: Lunch | |
| Chair: He Jifeng | |
| 14:00-14:30 | Keynote: Thomas Ball, Microsoft Research The Verified Software Challenge: A call for a holistic approach to reliability |
| 14:30-14:45 | Rajeev Joshi, NASA/JPL Laboratory for Reliable Software A Mini Grand Challenge: Build a Verifiable Filesystem |
| 14:45-15:00 | Cordell Green, Kestrel Institute A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets |
| 15:00-15:15 | Cliff Jones, Newcastle University What can we do (technically) to get "the right specification"? |
| 15:15-15:30 | Summary/Discussion |
| 15:30-16:00: Coffee Break | |
| 16:00-17:00 | Panel: Challenge Codes Bertrand Meyer, Willem Paul de Roever, Bernhard Steffen, Colin O'Halloran, Michael Butler Moderator: Jim Woodcock |
| 17:00-18:00 | Discussion |
| 18:00-: Welcome Buffet | |
Tuesday, Oct. 11th, 2005
| Time | Talk/Event |
|---|---|
| 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:15-10:30 | Summary/Discussion |
| 10:30-11:00: Coffee Break | |
| Chair: Masami Hagiya | |
| 11:00-11:30 | Keynote: Tom Reps, University of Wisconsin Interprocedural analysis, and some remaining challenges |
| 11:30-11:45 | Peter Müller, ETH Zürich Reasoning about Object Structures Using Ownership |
| 11:45-12:00 | David Naumann, Stevens Institute of Technology Modular Reasoning in Object-Oriented Programming |
| 12:00-12:15 | Peter O'Hearn, Queen Mary University of London Scalable Specification and Reasoning: Challenges for Program Logic |
| 12:15-12:30 | Summary/Discussion |
| 12:30-12:45: Free time | |
| 12:45-14:00: Lunch | |
| Chair: Panagiotis Manolios | |
| 14:00-14:30 | Keynote: Greg Nelson, HP SRC Classic, Palo Alto Extended static checking |
| 14:30-14:45 | Gary Leavens, Iowa State University Lessons from the JML project |
| 14:45-15:00 | Wolfram Schulte, Rustan Leino, Microsoft Research The Spec# Programming System: Challenges and Directions |
| 15:00-15:15 | Joseph Kiniry, University College Dublin Integrating Static Checking and Interactive Verification |
| 15:15-15:30 | Summary/Discussion |
| 15:30-16:00: Coffee Break | |
| 16:00-17:00 | Panel: Methodologies Moderator: Wolfram Schulte |
| 17:00-18:00 | Discussion |
Wednesday, Oct. 12th, 2005
| Time | Talk/Event |
|---|---|
| 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:15-10:30 | Summary/Discussion |
| 10:30-11:00: Coffee Break | |
| Chair: Ganesan Ramalingam | |
| 11:00-11:30 | Keynote: Patrick Cousot, École normale supérieure, Paris The Verification Grand Challenge and Abstract Interpretation |
| 11:30-11:45 | Tom Reps, University of Wisconsin Static Analysis of Executables |
| 11:45-12:00 | Martin Rinard, Massachusetts Institute of Technology Implications of a Data Structure Consistency Checking System |
| 12:00-12:15 | Arnaud Venet, Kestrel Technology LLC Towards a Homology Theory for Static Analysis |
| 12:15-12:30 | Summary/Discussion |
| 12:30-12:45: Free time | |
| 12:45-14:00: Lunch | |
| Chair: Marsha Chechik | |
| 14:00-14:30 | Keynote: Gerard Holzmann, NASA/JPL Laboratory for Reliable Software Reliable Software Systems Design |
| 14:30-14:45 | Rajeev Alur, University of Pennsylvania Trends and Challenges in Algorithmic Software Verification |
| 14:45-15:00 | Helmut Veith, TU München Model Checking: Back and Forth Between Hardware and Software |
| 15:00-15:15 | Grigore Rosu, University of Illinois at Urbana-Champaign Computational Logical Framework and Generic Program Analysis Technologies |
| 15:15-15:30 | Summary/Discussion |
| 15:30-16:00: Coffee Break | |
| 16:00-17:00 | Panel: Proof Tools Tevfik Bultan, Daniel Kröning, Tiziana Margaria, Harald Ruess, Ofer Strichman, Aaron Stump Moderator: Natarajan Shankar |
| 17:00-18:00 | Discussion |
Evening Program: Conference Dinner
Thursday, Oct. 13th, 2005
| Time | Talk/Event |
|---|---|
| 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:15-12:30 | Summary/Discussion |
| 12:30-12:45: Free time | |
| 12:45-14:00: Lunch | |
| 14:00-16:00 | Panel: Milestones and Road Map Greg Nelson, Rajeev Joshi, Peter O'Hearn, Joseph Kiniry, J Moore, Natarajan Shankar Moderator: Tony Hoare and Jayadev Misra |
!!! Dieses Dokument stammt aus dem ETH Web-Archiv und wird nicht mehr gepflegt !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!