9.00-17.30	Tutorial 1: Building, Combining, and Integrating Decision Procedures for Software Verification
9.00-17.30	Tutorial 2: Unified Modeling Language 2.0 - Concepts and Semantics
13.45-17.30	TRain workshop
19.30	TRain workshop dinner

8.45-17.30	TRain workshop
9.00-12.30	Tutorial 3: An Introduction to CSP||B
14.00-17.30	Tutorial 4: QoS Modelling and Verification with UML Statecharts

9.00-9.30	Opening Session
9.30-10.30	Keynote Talk 1  (Chair: Bernhard Beckert)
Wolfgang J. Paul	Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctness
11.00-12.30	Session 1A: Testing  (Chair: Anthony Hall)
Arshad Jhumka, Martin Hiller	Putting Detectors in their Place
Rita Dorofeeva, Khaled El-Fakih, Stephane Maag, Ana Cavalli, Nina Yevtushenko	Experimental Evaluation of FSM-Based Testing Methods
Mark Trakhtenbrot	Use of Verification Techniques for Testing and Debugging of Complex Reactive Systems
11.00-12.30	Session 1B: Real-time Systems  (Chair: Joseph Sifakis)
Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina	Timed Automata with Data Structures for Distributed Systems Design and Analysis
Xiuli Sun, Jinzhao Wu	Operational Semantics for Real-Time Processes with Action Refinement
Biniam Gebremichael, Frits Vaandrager	Specifying Urgency in Timed I/O Automata
14.00-15.00	Keynote Talk 2  (Chair: Bernhard Aichernig)
Dines Bjørner	A Cloverleaf of Software Engineering
15.30-17.00	Session 2A: Static Analysis  (Chair: Wolfgang Ahrendt)
Gilles Barthe, Mariela Pavlova, Gerardo Schneider	Static Analysis of Memory Consumption Using Program Logics
Mahadevan Subramaniam, Jiangfan Shi	Using Graph Dominators to Extract Observable Protocol Contexts
Ernesto Wandeler, Jörn Janneck, Edward Lee, Lothar Thiele	Counting Interface Automata and their Application in Static Analysis of Actor Models
15.30-17.00	Session 2B: Requirements and Specification  (Chair: Werner Stephan)
Frederic Gervais, Marc Frappier, Regine Laleau	Generating Relational Database Transactions From Recursive Functions Defined on EB3 Traces
Zsolt Nemeth, Christian Perez, Thierry Priol	Workflow Enactment Based on a Chemical Metaphor
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte	Safe Concurrency for Aggregate Objects with Invariants
17.30	Welcome reception / Opening International Conference Summer

9.00-10.00	Keynote Talk 3  (Chair: Peter Schmitt)
K. Rustan M. Leino	Invariants on Demand
10.00-10.30	Session 3: Program Verification I  (Chair: Peter Schmitt)
Thomas Wilson, Savi Maharaj, Robert Clark	Omnibus Verification Policies
11.00-12.30	Session 4A: Program Verification II  (Chair: Patrice Chalin)
Kerry Trentelman	Proving Correctness of JavaCard DL Taclets using Bali
Holger Grandy, Kurt Stenzel, Wolfgang Reif	Object Oriented Verification Kernels for Secure Java Applications
Ola Olsson, Angela Wallenburg	Customised Induction Rules for Proving Correctness of Imperative Programs
11.00-12.30	Session 4B: True Concurrency  (Chair: Antonio Cerone)
Jin Naiyong, Jifeng He	Towards a Truly Concurrent Model for Processes Sharing Resources
Joseph Kuehn, Charles Lakos, Robert Esser	A Proposal for Relative Time Petri Nets
Tarek Sadani, Jean-Pierre Courtiat, Pierre de Saqui-Sannes	From RT-LOTOS to Time Petri Nets: New Foundations for a Verification Platform
14.00-15.00	The FME Lecture - Keynote Talk 4  (Chair: Mike Hinchey)
Anthony Hall	Making Formal Methods Work
15.30-17.00	Session 5A: Program Verification III  (Chair: Zhiming Liu)
Thierry Hubert, Claude Marche	A Case Study of C Source Code Verification: The Schorr-Waite Algorithm
Jan Blech, Lars Gesellensetter, Sabine Glesner	Formal Verification of Dead Code Elimination in Isabelle/HOL
Hans de Nivelle, Ruzica Piskac	Verification of a Checker for Priority Queues
15.30-17.00	Session 5B: Formal Methods for Maintenance and Change  (Chair: Jürgen Ebert)
Zoltan Pap, Gyula Csopaki, Sarolta Dibuz	On the Theory of Patching
Jan Scheffczyk, Uwe Borghoff, Andreas Birk, Johannes Siedersleben	Pragmatic Consistency Management in Industrial Requirements Specifications
James Welch, David Faitelson, Jim Davies	Automatic Maintenance of Association Invariants
17.15	Excursion: Fortress Ehrenbreitstein
19.00	Conference dinner

9.00-10.00	Keynote Talk 5  (Chair: Andrea Maggiolo Schettini)
Joseph Sifakis	A Framework for Component-based Construction
10.00-10.30	Session 6: Program Verification IV  (Chair: Andrea Maggiolo Schettini)
Wishnu Prasetya, Ade Azurat, Tanja Vos, Arthur van Leeuwen	Building Verification Condition Generators by Compositional Extensions
11.00-12.30	Session 7A: Abstraction  (Chair: Rustan Leino)
Mila Dalla Preda, Roberto Giacobazzi	Control Code Obfuscation by Abstract Interpretation
Marsha Chechik, Arie Gurfinkel, Shiva Nejati	Stuttering Abstraction for Model Checking
Lilia Georgieva, Patrick Maier	Description Logics for Shape Analysis
11.00-12.30	Session 7B: Human-Computer Interaction  (Chair: Martin Wirsing)
Hui Shi, Robert Ross, John Bateman	Formalising Control in Robust Spoken Dialogue Systems
Anke Dittmar, Peter Forbrig	A Unified Description Formalism for Complex HCI-Systems
Antonio Cerone, Peter Lindsay, Simon Connelly	Formal Analysis of Human-Computer Interaction Using Model-checking
14.00-15.30	Session 8A: Tools and Practice  (Chair: Shmuel Tyszberowicz)
Gareth Carter, Rosemary Monahan, Joseph Morris	Software Refinement with Perfect Developer
Samuel Colin, Dorian Petit, Jerome Rocheteau, Rafael Marcano, Georges Mariano, Vincent Poirriez	BRILLANT: An Open Source and XML-based Platform for Rigourous Software Development
Patrice Chalin	Logical Foundation of Program Assertions: What do Practitioners Want?
14.00-15.30	Session 8B: Component-based Development  (Chair: Dines Bjørner)
Dan Hirsch, Emilio Tuosto	SHReQ: Coordinating Application Level QoS
Walter Mesquita, Augusto Sampaio, Ana C. V. de Melo	A Strategy for the Formal Composition of Frameworks
Dilian Gurov, Marieke Huisman	Interface Abstraction for Compositional Verification
15.30-16.00	Closing Session