default search action
FM 2011: Limerick, Ireland
- Michael J. Butler, Wolfram Schulte:
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
Cyber-Physical Systems
- 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
Runtime Analysis
- 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
Case Studies / Tools
- Fabienne Boyer, Olivier Gruber, Gwen Salaün:
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP. 103-117 - Anne E. 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
Experience
- Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß:
The 1st Verified Software Competition: Experience Report. 154-168
Program Compilation and Transformation
- 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
Security
- 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
Process Algebra
- 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
Education
- 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
Concurrency
- 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
Dynamic Structures
- 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
Model Checking
- 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.