Program verification has seen a worldwide renaissance, with many practical tool projects and experimental verification efforts ongoing. The current state of the field builds on fundamental theoretical advances of the past. Similarly, future advances on software verification will depend on developments in theory. This can range from the difficult and essential study of soundness of delicate proof methods, to the discovery of new specification techniques and proof methods, to dramatic simplification or unification of existing methods, to as yet unknown breakthroughs.
The Verified Software Initiative (VSI) is envisaged as a fifteen year ``grand challenge'' project to advance the state of software verification. Specific milestones and challenges of the VSI should often be concrete in nature, but advances beyond immediate progress will again depend on theoretical insights. The purpose of this workshop is to bring together theory and programming language researchers to discuss scientific challenges posed by software verification.
10:30
Andrey Rybalchenko, Max Planck Institute
Joining forces to verify programs
11:20
Carroll Morgan, University of New South Wales
A calculus of revelations
12:10 Discussion: what are the major open problems in theory?
12:30 Lunch
2:00
Xavier Rival, INRIA
Design of parametric abstract domains for shape analysis
2:50
Aleksandar Nanevski, Microsoft Research
Program verification with Hoare Type Theory
3:40 Break
4:00
Philippa Gardiner, Imperial College
Local Hoare reasoning about DOM
4:50
Hongseok Yang, Queen Mary, University of London
Local reasoning for Read-Copy-Update
5:40 Five-minute one-slide talks -- please contact organizers.
The THEORY Workshop is part of VSTTE 2008, which will take place in Toronto, Canada.
| Dave Naumann | Peter O'Hearn | |
| Stevens Institute of Technology | Queen Mary, University of London | |
| naumann cs.stevens.edu | ohearn dcs.qmul.ac.uk |