This book constitutes the refereed proceedings of the 8th International Conference on Integrated Formal Methods, IFM 2010, held in Nancy, France, in October 2010. The 20 revised full papers presented together with 3 invited papers were carefully reviewed and selected from 59 submissions. The papers address the spectrum of integrated formal methods, ranging from formal and semiformal notations, semantics, refinement, verification and model transformations to type systems, logics, tools and case studies.
Author(s): Christel Baier (auth.), Dominique Méry, Stephan Merz (eds.)
Series: Lecture Notes in Computer Science 6396 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 337
Tags: Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Mathematical Logic and Formal Languages; Programming Techniques; Algorithm Analysis and Problem Complexity
Front Matter....Pages -
On Model Checking Techniques for Randomized Distributed Systems....Pages 1-11
Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems....Pages 12-26
Programming with Miracles....Pages 27-27
An Event-B Approach to Data Sharing Agreements....Pages 28-42
A Logical Framework to Deal with Variability....Pages 43-58
Adding Change Impact Analysis to the Formal Verification of C Programs....Pages 59-73
Creating Sequential Programs from Event-B Models....Pages 74-88
Symbolic Model-Checking of Optimistic Replication Algorithms....Pages 89-104
From Operating-System Correctness to Pervasively Verified Applications....Pages 105-120
A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs....Pages 121-135
Verification Architectures: Compositional Reasoning for Real-Time Systems....Pages 136-151
Automatic Verification of Parametric Specifications with Complex Topologies....Pages 152-167
Satisfaction Meets Expectations....Pages 168-182
Showing Full Semantics Preservation in Model Transformation - A Comparison of Techniques....Pages 183-198
Specification and Verification of Model Transformations Using UML-RSDS....Pages 199-214
Multiformalism and Transformation Inheritance for Dependability Analysis of Critical Systems....Pages 215-228
Translating Pi-Calculus into LOTOS NT....Pages 229-244
Systematic Translation Rules from astd to Event-B....Pages 245-259
A CSP Approach to Control in Event-B....Pages 260-274
Towards Probabilistic Modelling in Event-B....Pages 275-289
Safe Commits for Transactional Featherweight Java....Pages 290-304
Certified Absence of Dangling Pointers in a Language with Explicit Deallocation....Pages 305-319
Integrating Implicit Induction Proofs into Certified Proof Environments....Pages 320-335
Back Matter....Pages -