fm2011 / Main Conference

lero — Wed, 15 Jun 2011 11:47:29 GMT

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

lero RSS Feed

fm2011 / Main Conference