FM 2012: Formal Methods: 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings

Front Matter....Pages -
Software Security: A Formal Perspective....Pages 1-5
Formal Methods in the Wild: Trains, Planes, & Automobile....Pages 6-6
Who Are We, and What Are We Doing Here?....Pages 7-9
Automata Learning through Counterexample Guided Abstraction Refinement....Pages 10-27
 Julienne : A Trace Slicer for Conditional Rewrite Theories....Pages 28-32
IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems....Pages 33-36
Maximal and Compositional Pattern-Based Loop Invariants....Pages 37-51
A Formal Approach to Autonomous Vehicle Coordination....Pages 52-67
Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors....Pages 68-84
Decentralised LTL Monitoring....Pages 85-100
Measles Epidemics and PEPA: An Exploration of Historic Disease Dynamics Using Process Algebra....Pages 101-115
A Certified Constraint Solver over Finite Domains....Pages 116-131
Collaborative Verification and Testing with Explicit Assumptions....Pages 132-146
TLA  +  Proofs....Pages 147-154
The Modal Transition System Control Problem....Pages 155-170
When Structural Refinement of Components Keeps Temporal Properties over Reconfigurations....Pages 171-186
Error Invariants....Pages 187-201
Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction....Pages 202-216
A Formal Framework for Modelling Coercion Resistance and Receipt Freeness....Pages 217-231
Using Time to Add Order to Distributed Testing....Pages 232-246
A Verification Toolkit for Numerical Transition Systems....Pages 247-251
Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems....Pages 252-266
Executing Formal Semantics with the $\mathbb K$ Tool....Pages 267-271
Automatic Compositional Verification of Timed Systems....Pages 272-276
Applying Software Model Checking Techniques for Behavioral UML Models....Pages 277-292
Reachability Analysis of the HTML5 Parser Specification and Its Application to Compatibility Testing....Pages 293-307
Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms....Pages 308-325
Improved BDD-Based Discrete Analysis of Timed Systems....Pages 326-340
Experience Report on Designing and Developing Control Components Using Formal Methods....Pages 341-355
Automatic Dimensional Analysis of Cyber-Physical Systems....Pages 356-371
Validating B,Z and TLA  +  Using ProB  and Kodkod....Pages 372-386
From Hoare Logic to Matching Logic Reachability....Pages 387-402
Distribution of Modal Transition Systems....Pages 403-417
Efficient Malware Detection Using Model-Checking....Pages 418-433
Formalization of Incremental Simplex Algorithm by Stepwise Refinement....Pages 434-449
VMC: A Tool for Product Variability Analysis....Pages 450-454
Specification-Based Test Repair Using a Lightweight Formal Method....Pages 455-470
A “Hybrid” Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example....Pages 471-485
Back Matter....Pages -