Software Engineering and Formal Methods: 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014. Proceedings

✍ Scribed by Dimitra Giannakopoulou, Gwen Salaün (eds.)

• Publisher: Springer International Publishing
• Year: 2014
• Tongue: English
• Leaves: 412
• Series: Lecture Notes in Computer Science 8702 Programming and Software Engineering
• Edition: 1
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

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 -

✦ Subjects

Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Mathematical Logic and Formal Languages; Computer Communication Networks; Programming Techniques