Integrated Formal Methods

1. Front Matter

   PDF

2. Invited Paper 1

   1. From Z to B and then Event-B: Assigning Proofs to Meaningful Programs

      • Jean-Raymond Abrial

      Pages 1-15

   2. Refinement, Integration, Translation

      1. Systems Design Guided by Progress Concerns

         • Simon Hudon, Thai Son Hoang

         Pages 16-30

      2. Assume-Guarantee Specifications of State Transition Diagrams for Behavioral Refinement

         • Christian Prehofer

         Pages 31-45

      3. Translating VDM to Alloy

         • Kenneth Lausdahl

         Pages 46-60

      4. Verification of EB3 Specifications Using CADP

         • Dimitris Vekris, Frédéric Lang, Catalin Dima, Radu Mateescu

         Pages 61-76

3. Invited Paper 2

   1. Knowledge for the Distributed Implementation of Constrained Systems

      • Susanne Graf, Sophie Quinton

      Pages 77-93

   2. Verification

      1. Automated Anonymity Verification of the ThreeBallot Voting System

         • Murat Moran, James Heather, Steve Schneider

         Pages 94-108

      2. Compositional Verification of Software Product Lines

         • Jean-Vivien Millo, S. Ramesh, Shankara Narayanan Krishna, Ganesh Khandu Narwane

         Pages 109-123

      3. Deductive Verification of State-Space Algorithms

         • Frédéric Gava, Jean Fortin, Michael Guedj

         Pages 124-138

      4. Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus

         • Daisuke Ishii, Guillaume Melquiond, Shin Nakajima

         Pages 139-153

4. Invited Paper 3

   1. Priced Timed Automata and Statistical Model Checking

      • Kim Guldstrand Larsen

      Pages 154-161

   2. Reachability and Model Checking

      1. Improved Reachability Analysis in DTMC via Divide and Conquer

         • Songzheng Song, Lin Gui, Jun Sun, Yang Liu, Jin Song Dong

         Pages 162-176

      2. Solving Games Using Incremental Induction

         • Andreas Morgenstern, Manuel Gesell, Klaus Schneider

         Pages 177-191

      3. Model-Checking Software Library API Usage Rules

         • Fu Song, Tayssir Touili

         Pages 192-207

      4. Formal Modelling and Verification of Population Protocols

         • Dominique Méry, Michael Poppleton

         Pages 208-222

   3. Usability and Testing

      1. Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based Testing

         • Aymerick Savary, Marc Frappier, Jean-Louis Lanet

         Pages 223-237

      2. Integrating Formal Predictions of Interactive System Behaviour with User Evaluation

         • Rimvydas Rukšėnas, Paul Curzon, Michael D. Harrison

         Pages 238-252

      3. Automatic Inference of Erlang Module Behaviour

         • Ramsay Taylor, Kirill Bogdanov, John Derrick

         Pages 253-267

   4. Distributed Systems

      1. Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms

         • Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh

         Pages 268-284

This book constitutes the refereed proceedings of the 10th International Conference on Integrated Formal Methods, IFM 2013, held in Turku, Finland, in June 2013.
The 25 revised full papers presented together with 4 invited papers were carefully reviewed and selected from 84 full paper submissions. The papers cover the spectrum of integrated formal methods, focusing on refinement, integration, translation, verification, reachability and model checking, usability and testing, distributed systems, semantics, and system-level analysis.

• complex systems
• distributed algorithms
• hybrid automata
• model-based testing
• state machines

• Department of Informatics, University of Oslo, Oslo, Norway

  Einar Broch Johnsen

• Department of Information Technologies, Åbo Akademi University, Turku, Finland

  Luigia Petre

Policies and ethics