Software Engineering and Formal Methods

1. Front Matter

   PDF

2. Invited Papers

   1. Formal Proofs of Code Generation and Verification Tools

      • Xavier Leroy

      Pages 1-4

3. Program Verification

   1. Lightweight Program Construction and Verification Tools in Isabelle/HOL

      • Alasdair Armstrong, Victor B. F. Gomes, Georg Struth

      Pages 5-19

   2. Completeness of Separation Logic with Inductive Definitions for Program Verification

      • Makoto Tatsuta, Wei-Ngan Chin

      Pages 20-34

   3. A Thread-Safe Library for Binary Decision Diagrams

      • Alberto Lovato, Damiano Macedonio, Fausto Spoto

      Pages 35-49

   4. Effect-Polymorphic Behaviour Inference for Deadlock Checking

      • Ka I Pun, Martin Steffen, Volker Stolz

      Pages 50-64

4. Testing

   1. Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations

      • Maria Christakis, Peter Müller, Valentin Wüstholz

      Pages 65-80

   2. Formalizing DSL Semantics for Reasoning and Conformance Testing

      • Sarmen Keshishzadeh, Arjan J. Mooij

      Pages 81-95

   3. Test Suite Completeness and Partial Models

      • Adilson Luiz Bonifacio, Arnaldo Vieira Moura

      Pages 96-110

5. Component-Based Systems

   1. Automated Error-Detection and Repair for Compositional Software Specifications

      • Dalal Alrajeh, Robert Craven

      Pages 111-127

   2. A General Framework for Architecture Composability

      • Paul Attie, Eduard Baranov, Simon Bliudze, Mohamad Jaber, Joseph Sifakis

      Pages 128-143

   3. Trace Checking of Metric Temporal Logic with Aggregating Modalities Using MapReduce

      • Domenico Bianculli, Carlo Ghezzi, Srđan Krstić

      Pages 144-158

6. Real-Time and Embedded Systems

   1. Increasing Consistency in Multi-site Data Stores: Megastore-CGC and Its Formal Analysis

      • Jon Grov, Peter Csaba Ölveczky

      Pages 159-174

   2. Evaluating the Effect of Faults in SystemC TLM Models Using UPPAAL

      • Reza Hajisheykhi, Ali Ebnenasir, Sandeep S. Kulkarni

      Pages 175-189

   3. Formal Verification of Discrete-Time MATLAB/Simulink Models Using Boogie

      • Robert Reicherdt, Sabine Glesner

      Pages 190-204

   4. A Formal Model for Constraint-Based Deployment Calculation and Analysis for Fault-Tolerant Systems

      • Klaus Becker, Bernhard Schätz, Michael Armbruster, Christian Buckl

      Pages 205-219

7. Model Checking and Automata Learning

   1. Optimising the ProB Model Checker for B Using Partial Order Reduction

      • Ivaylo Dobrikov, Michael Leuschel

      Pages 220-234

   2. Rapid Prototyping of a Semantically Well Founded Circus Model Checker

      • Alexandre Mota, Adalberto Farias, André Didier, Jim Woodcock

      Pages 235-249

   3. Learning Extended Finite State Machines

      • Sofia Cassel, Falk Howar, Bengt Jonsson, Bernhard Steffen

      Pages 250-264

8. Tool Papers

   1. Translating Event-B Machines to Database Applications

      • Qi Wang, Tim Wahls

      Pages 265-270

This book constitutes the refereed proceedings of the 12th International Conference on Software Engineering and Formal Methods, SEFM 2014, held in Grenoble, France, in September 2014.
The 23 full papers presented together with 3 invited and 6 tool papers were carefully reviewed and selected from 106 submissions. They are organized in topical section on program verification, testing, component-based systems, real-time and embedded systems, model checking and automata learning, program correctness, and adaptive and multi-agent systems.

• adaptive systems
• automata learning
• automated static analysis
• component-based systems
• dynamic analysis
• embedded systems
• formal methods
• model checking
• multi-agent systems
• ontology
• program correctness
• real-time systems
• requirements engineering
• software engineering
• software testing and debugging
• software verification
• software verification and validation
• temporal logic
• theorem proving
• verification

• NASA Ames Research Center, USA

  Dimitra Giannakopoulou

• Inria Grenoble-Rhône-Alpes, Montbonnot Saint-Martin, France

  Gwen Salaün

Policies and ethics