Software engineering and formal methods : 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014 : proceedings

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. Front Matter....Pages - Formal Proofs of Code Generation and Verification Tools....Pages 1-4 Lightweight Program Construction and Verification Tools in Isabelle/HOL....Pages 5-19 Completeness of Separation Logic with Inductive Definitions for Program Verification....Pages 20-34 A Thread-Safe Library for Binary Decision Diagrams....Pages 35-49 Effect-Polymorphic Behaviour Inference for Deadlock Checking....Pages 50-64 Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations....Pages 65-80 Formalizing DSL Semantics for Reasoning and Conformance Testing....Pages 81-95 Test Suite Completeness and Partial Models....Pages 96-110 Automated Error-Detection and Repair for Compositional Software Specifications....Pages 111-127 A General Framework for Architecture Composability....Pages 128-143 Trace Checking of Metric Temporal Logic with Aggregating Modalities Using MapReduce....Pages 144-158 Increasing Consistency in Multi-site Data Stores: Megastore-CGC and Its Formal Analysis....Pages 159-174 Evaluating the Effect of Faults in SystemC TLM Models Using UPPAAL....Pages 175-189 Formal Verification of Discrete-Time MATLAB/Simulink Models Using Boogie....Pages 190-204 A Formal Model for Constraint-Based Deployment Calculation and Analysis for Fault-Tolerant Systems....Pages 205-219 Optimising the ProB Model Checker for B Using Partial Order Reduction....Pages 220-234 Rapid Prototyping of a Semantically Well Founded Circus Model Checker....Pages 235-249 Learning Extended Finite State Machines....Pages 250-264 Translating Event-B Machines to Database Applications....Pages 265-270 IKOS: A Framework for Static Analysis Based on Abstract Interpretation....Pages 271-277 A Toolset for Support of Teaching Formal Software Development....Pages 278-283 Execution and Verification of UML State Machines with Erlang....Pages 284-289 A Tool for Verifying Dynamic Properties in B....Pages 290-295 WeVerca: Web Applications Verification for PHP....Pages 296-301 More Flexible Object Invariants with Less Specification Overhead....Pages 302-316 Verified Functional Iterators Using the FoCaLiZe Environment....Pages 317-331 Tool Support for Teaching Hoare Logic....Pages 332-346 A Two-Phase Static Analysis for Reliable Adaptation....Pages 347-362 Formal Modelling and Verification of Cooperative Ant Behaviour in Event-B....Pages 363-377 A Formal Privacy Policy Framework for Social Networks....Pages 378-392 Back Matter....Pages -