VERIFY program

All sessions take place in auditorium 6.

Thursday July 25th

Thursday's program is also available with abstracts or side by side with other meetings.

08:45-10:30  Session 1: Applications of ATP in Verification

08:45  Welcoming and Opening Remarks
09:00  Daniel Kröning, Carnegie Mellon U, USA
Application specific higher order logic theorem proving
09:30  Vincent Vanackère, Provence U, Marseille, France
The TRUST protocol analyser, automatic and efficient verification of cryptographic protocols
10:00  Christoph Benzmüller, Saarland U, Germany; Corrado Giromini, Saarland U, Germany; Andreas Nonnengart, DFKI Saarbrücken, Germany; and Jürgen Zimmer, Saarland U, Germany
Reasoning services in MathWeb-SB for symbolic verification of hybrid systems

10:30-11:00  Refreshments

11:00-12:30  Session 2: Logical Approaches (joint with FCS)
Chair: Catherine Meadows

11:00  Andrew W. Appel, Princeton U, USA; Neophytos G. Michael, Princeton U, USA; Aaron Stump, Stanford U, USA; and Roberto Virga, Princeton U, USA
A trustworthy proof checker
11:30  Ernie Cohen, Microsoft Research Cambridge, UK
Proving protocols safe from guessing
12:00  Alessandro Armando and Luca Compagna, U Genova, Italy
Automatic SAT-compilation of security problems

12:30-14:00  Lunch

14:00-15:30  Session 3: VERIFY Invited talk (joint with FCS)
Chair: Heiko Mantel

14:00  Fabio Massacci, U Trento, Italy
Invited talk: Formal verification of SET by Visa and Mastercard: Lessons for formal methods in security

15:30-16:00  Refreshments

16:00-17:00  Session 4: Verification of Security Protocols (joint with FCS)
Chair: Dieter Gollmann

16:00  Catherine Meadows, Naval Research Laboratory, USA
Identifying potential type confusion in authenticated messages
16:30  Graham Steel, Alan Bundy, and Ewen Denney; U Edinburgh, UK
Finding counterexamples to inductive conjectures and discovering security protocol attacks

Friday July 26th

Friday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 5: FCS Invited talk (joint with FCS)
Chair: Iliano Cervesato

09:00  Dieter Gollmann, Microsoft Research Cambridge, UK
Invited talk: Defining security is difficult and error prone

10:30-11:00  Refreshments

11:00-12:30  Session 6: Specification and Verification

11:00  Amy L. Herzog and Joshua Guttman, MITRE, USA
Eager formal methods for security management
11:30  Alessandro Armando, U Genova, Italy; Maria Paola Bonacina, U Iowa, USA; Silvio Ranise, LORIA Nancy, France; Michaël Rusinowitch, LORIA Nancy, France; and Aditya Kumar Sehgal, U Iowa, USA
High-performance deduction for verification: a case study in the theory of arrays
12:00  Bernhard Beckert, Uwe Keller, and Peter H. Schmitt; Karlsruhe U, Germany
Translating the object constraint language into first-order predicate logic

12:30-14:00  Lunch

14:00-15:40  Session 7 (joint with FCS)
Chair: Serge Autexier, Iliano Cervesato, Heiko Mantel

14:00  Ernie Cohen, Microsoft Research Cambridge, UK; Alan Jeffrey, DePaul U, USA; Fabio Martinelli, CNR Pisa, Italy; Fabio Massacci, U Trento, Italy; Catherine Meadows, Naval Research Laboratory, USA; and David Basin, U Freiburg, Germany
Panel: The future of protocol verification
15:30  Closing Remarks