FM 2011: Limerick, Ireland

Michael Butler, Wolfram Schulte (Eds.): FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings. Lecture Notes in Computer Science 6664 Springer 2011, ISBN 978-3-642-21436-3

Invited Talks

Janos Sztipanovits:
Model Integration and Cyber Physical Systems: A Semantics Perspective. 1
David Harel:
Some Thoughts on Behavioral Programming. 2
Jasmin Fisher, Nir Piterman, Moshe Y. Vardi:
The Only Way Is Up. 3-11

Werner Damm, Bernd Finkbeiner:
Does It Pay to Extend the Perimeter of a World Model? 12-26
Daniel Dietsch, Bernd Westphal, Andreas Podelski:
System Verification through Program Verification. 27-41
Sarah M. Loos, André Platzer, Ligia Nistor:
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. 42-56

Howard Barringer, Klaus Havelund:
TraceContract: A Scala DSL for Trace Analysis. 57-72
Peter Müller, Joseph N. Ruskiewicz:
Using Debuggers to Understand Failed Verification Attempts. 73-87
Borzoo Bonakdarpour, Samaneh Navabpour, Sebastian Fischmeister:
Sampling-Based Runtime Verification. 88-102

Fabienne Boyer, Olivier Gruber, Gwen Salaün:
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP. 103-117
Anne Elisabeth Haxthausen, Andreas A. Kjær, Marie Le Bliguet:
Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems. 118-132
Aboubakr Achraf El Ghazi, Mana Taghdiri:
Relational Reasoning via SMT Solving. 133-148
Nuno Amálio, Christian Glodt, Pierre Kelsen:
Building VCL Models and Automatically Generating Z Specifications from Them. 149-153

Guodong Li:
Validated Compilation through Logic. 169-183
Javier de Dios, Ricardo Peña:
Certification of Safe Polynomial Memory Bounds. 184-199
Gilles Barthe, Juan Manuel Crespo, César Kunz:
Relational Verification Using Product Programs. 200-214

Michael J. Banks, Jeremy L. Jacob:
Specifying Confidentiality in Circus. 215-230
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna:
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. 231-245
Ana Cavalcanti, Andy J. Wellings, Jim Woodcock:
The Safety-Critical Java Memory Model: A Formal Account. 246-261

Zhenbang Chen, Zhiming Liu, Ji Wang:
Failure-Divergence Refinement of Compensating Communicating Processes. 262-277
Steve Dunne:
Termination without \checkmark\checkmark in CSP. 278-292
Gabriel Ciobanu, Maciej Koutny:
Timed Migration and Interaction with Access Permissions. 293-307

Jonathan P. Bowen, Steve Reeves:
From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods Community. 308-322

John Derrick, Gerhard Schellhorn, Heike Wehrheim:
Verifying Linearisability with Potential Linearisation Points. 323-337
Dominique Méry, Mohamed Mosbah, Mohamed Tounsi:
Refinement-Based Verification of Local Synchronization Algorithms. 338-352
Elvira Albert, Samir Genaim, Miguel Gómez-Zamalloa, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa:
Simulating Concurrent Behaviors with Worst-Case Cost Bounds. 353-368

Shengchao Qin, Chenguang Luo, Wei-Ngan Chin, Guanhua He:
Automatically Refining Partial Specifications for Program Verification. 369-385
Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin:
Structured Specifications for Better Verification of Heap-Manipulating Programs. 386-401
Bart Jacobs, Jan Smans, Frank Piessens:
Verification of Unloadable Modules. 402-416

Kristin Y. Rozier, Moshe Y. Vardi:
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. 417-431
Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong:
On Combining State Space Reductions with Global Fairness Assumptions. 432-447

Last update Fri May 25 08:14:13 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page