FLoC '02 - VERIFY program

VERIFY program

All sessions take place in auditorium 6.

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

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'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