Wednesday 22 June

09:00 - 09:30 Opening Address

09:30 - 10:30 Invited Talk I

Janos Sztipanovits. Model Integration and Cyber Physical Systems:  A Semantics Perspective.

10:30 - 11:00 Coffee

11:00 - 12:30 Cyber Physical Systems

Does It Pay to Extend the Perimeter of a World Model? Damm, Finkbeiner.

System Verification Through Program Verification. Dietsch, Westphal, Podelski.

Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. Loos, Platzer, Nistor.

12:45 - 14:00 Lunch

14:00 - 15:30 Runtime Analysis

TraceContract: A Scala DSL for Trace Analysis. Barringer, Havelund.

Using Debuggers to Understand Failed Verification Attempts. Müller, Ruskiewicz.

Sampling-based Runtime Verification. Bonakdarpour, Navabpour, Fischmeister.

15:30 - 16:00 Coffee

16:00 - 17:45 Case Studies / Tools

Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT/CADP. Boyer, Gruber, Salaün.

Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems. Haxthausen, Kjaer, Le Bliguet.

Relational Reasoning via SMT Solving. El Ghazi, Taghdiri.

Building VCL Models and Automatically Generating Z Specifications From Them. Amalio, Glodt, Kelsen. (15 mins)

Thursday 23 June

09:00 - 10:00 Invited Talk II

David Harel. Some Thoughts on Behavioral Programming.

10:00 - 10:30 Experience Report

The 1st Verified Software Competition: Experience Report. Klebanov, Müller, N. Shankar, Leavens, Wüstholz, Alkassar, Arthan,
Bronish, Chapman, Cohen, Hillebrand, Jacobs, Leino, Monahan, Piessens, Polikarpova, Ridge, Smans, Tobies, Tuerk, Ulbrich, Weiß..

10:30 - 11:00 Coffee

11:00 - 12:30 Program Compilation and Transformation

Validated Compilation Through Logic. Li.

Certification of Safe Polynomial Memory Bounds. De Dios, Peña.

Relational Verification Using Product Programs. Barthe, Crespo, Kunz.

12:45 - 14:00 Lunch

14:00 - 15:30 Security

Specifying Confidentiality in Circus. Banks, Jacob.

Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. Barthe, Betarte, Campo, Luna.

The Safety-critical Java Memory Model:  a formal account. Cavalcanti, Woodcock, Wellings.

15:30 - 16:00 Coffee

16:00 -17:30 Process Algebra

Failure-Divergence Refinement of Compensating Communicating Processes. Chen, Liu, Wang.

Termination Without Tick in CSP. Dunne.

Timed Migration and Interaction with Access Permissions. Ciobanu, Koutny.

Friday 24 June

09:00 - 10:00 Invited Talk III

Jasmin Fisher. Executable Biology: Towards Computer Programmes That Mimic Life.

10:00 - 10:30 Education

From a Community of Practice to a Body of Knowledge: A case study of the formal methods community. Bowen, Reeves.

10:30 - 11:00 Coffee

11:00 - 12:30 Concurrency

Verifying Linearisability with Potential Linearisation Points.Derrick, Schellhorn, Wehrheim.

Refinement-based Verification of Local Synchronization Algorithms.Méry, Mosbah, Tounsi.

Simulating Concurrent Behaviors with Worst-Case Cost Bounds. Albert, Genaim, Gomez-Zamalloa, Johnsen, Schlatte, Tapia Tarifa.

12:45 - 13.00 FM12 Presentation

13.00 - 14:00 Lunch

14:00 - 15:30 Dynamic Structures

Automatically Refining Partial Specifications for Program Verification. Qin, Luo, Chin, He.

Structured Specifications for Better Verification of Heap-Manipulating Programs. Gherghina, David, Qin, Chin.

Verification of Unloadable Modules. Jacobs, Smans, Piessens.

15:30 - 16:00 Coffee

16:00 - 17:00 Model Checking

A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking.Rozier, Vardi.

On Combining State Space Reductions with Global Fairness Assumptions.Zhang, Sun, Pang, Liu, Dong.

17:00      Close