Mon (2/21/05): Verification Tools
9AM: Tony Hoare: The Verification Grand Challenge

10-10.30: COFFEE

10.30-11: Ed Clarke: Grand Challenge: Model Check Software

11-12: Model Checking: Allen EMERSON (emerson_at_cs.utexas.edu), Leonardo de Moura, Ed Clarke, Ken McMillan, Rupak Majumdar.

LUNCH

1 - 2PM: Software Model Checking: Gerard HOLZMANN, Matt Dwyer, Ganesh Gopalakrishnan , Wilhelm Visser, Sriram Rajamani

2-3PM: Decision procedures: Randy BRYANT, Lintao Zhang, Sergey Berezin, Rajeev Joshi, Harald Ruess, Nils Klarlund

COFFEE

3.30-4.30: Deduction: SHANKAR, Deepak Kapur, J Moore, Jose Meseguer, Konrad Slind, John Harrison

4.30-5.30: Discussion

9-9.30: Greg NELSON: Towards automatic verification: The ESC experience with program checking.

9.30-10: Bertrand MEYER: Formal basis for verifying object-oriented programs

10.30-12: Static/dynamic analysis: Alex AIKEN, David Evans, Dawson Engler, Henny Sipma, Scott McPeak, Klaus Havelund, Yuan Yu

LUNCH

1-2PM: Languages/Models/Semantics: Greg MORRISETT, John Reynolds, Dave Musser, Josh Tauber

2-3PM: Programming methodology: Jay MISRA, Daniel Jackson, Rustan Leino, Connie Heitmeyer, Doug Smith, Peter Homeier, Pete Manolios

COFFEE

3.30-4.30: Applications: John HARRISON , Paul Loewenstein, Rance DeLong, Bill Legato, Connie Heitmeyer, James Rash, Dave Hardin, Wolfram Schulte

4.30-5.30: Discussion

BANQUET 7--9PM

9: Amir Pnueli: Looking Ahead

9.30: Metrics/Milestones: Randy Bryant, Gerard Holzmann, Greg Nelson, Paul Black

11: Organization: Brad MARTIN, Helen Gill, Paul Black, Jay Misra, Tony Hoare

12 noon: LUNCH