Program

All sessions will take place in Suite 3128 unless otherwise indicated.

Tuesday, August 15th

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

09:00‑10:00  Session 1

09:00

John Rushby (SRI International) Threatened by a Great Opportunity: Disruptive Innovation in Formal Verification [pdf]

10:00‑10:30  Break

10:30‑12:00  Session 2: Verification Tools I

10:30	Myla Archer and Elizabeth Leonard Establishing High Confidence in Code Implementations of Algorithms using Formal Verification of Pseudocode
11:00	Robert Palmer , Ganesh Gopalakrishnan and Mike Kirby Formal Specification and Verification Using +CAL: An Experience Report
11:30	Bernhard Beckert and Vladimir Klebanov Must Program Verification Systems and Calculi be Verified?

12:30‑14:00  Lunch break

14:00‑15:30  Session 3: Verification Tools II

14:00	Sara Van Langenhove and Albert Hoogewijs Verifying Sliced Hierarchical Statecharts with SVtL
14:30	Laura Ildiko Kovacs and Tudor Jebelean Finding Polynomial Invariants for Imperative Loops in the Theorema System
15:00	Achim D. Brucker and Burkhart Wolff A Package for Extensible Object-Oriented Data Models with an Application to IMP++

15:30‑16:00  Break

16:00‑17:00  Session 4: Information Flow Security

16:00	Raghavendra Kagalavadi Ramesh and Deepak D'Souza Checking Unwinding Conditions for Finite State Systems
16:30	Dieter Hutter Automating Proofs of Unwinding Conditions

Wednesday, August 16th

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

09:30‑10:30  Session 5

09:30

Christoph Walther (TU Darmstadt) Verification in the Classroom

10:30‑11:00  Break

11:00‑12:30  Session 6: Security Protocols

11:00	Luca Vigano (ETH Zürich) Automated Reasoning for Security Protocol Analysis [pdf]
12:00	Siraj Shaikh , Vicky Bush and Steve Schneider A heuristic for constructing rank functions to verify authentication protocols

12:30‑14:00  Lunch break

14:30‑15:30  Session 7: Compositional & Modular Reasoning

14:30	Viorica Sofronie-Stokkermans Local reasoning in verification
15:00	Andreas Schlosser , Christoph Walther and Markus Aderhold Axiomatic Specifications in VeriFun

15:30‑16:00  Break

16:00‑18:00  Session 8: Panel discussion: "What are the verification problems? What are the deduction techniques?"