SEFM Conference Program
| September 3, 2014 (Wednesday) | |
|---|---|
| 08:45 – 09:00 | Opening |
| 09:00 – 10:00 | Invited speaker : Xavier Leroy Formal proofs of code generation and verification tools Session Chair: Gwen Salaün |
| 10:00 – 10:30 | Coffee break |
| 10:30 – 12:30 | Session 1 – Program Verification |
| Session Chair: Simon Bliudze | |
|
Alasdair Armstrong, Victor B. F. Gomes and Georg Struth. Lightweight Program Construction and Verification in Isabelle/HOL |
|
|
Makoto Tatsuta and Wei-Ngan Chin. Completeness of Separation Logic with Inductive Definitions for Program Verification |
|
|
Alberto Lovato, Damiano Macedonio and Fausto Spoto. A Thread-Safe Library for Binary Decision Diagrams |
|
|
Ka I Pun, Martin Steffen and Volker Stolz. Effect-Polymorphic Behaviour Inference for Deadlock Checking |
|
| 12:30 – 14:00 | Lunch |
| 14:00 – 15:30 | Session 2 – Testing |
| Session Chair: Dalal Alrajeh | |
|
Sarmen Keshishzadeh and Arjan Mooij. Formalizing DSL Semantics for Reasoning and Conformance Testing |
|
|
Maria Christakis, Peter Müller and Valentin Wüstholz. Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations |
|
|
Adilson Bonifacio and Arnaldo Moura. Test Suite Completeness and Partial Models |
|
| 15:30 – 16:00 | Coffee break |
| 16:00 – 17:30 | Session 3 – Component-Based Systems |
| Session Chair: Peter Olveczky | |
|
Dalal Alrajeh and Robert Craven. Automated Error-Detection and Repair for Compositional Software Specifications |
|
|
Paul Attie, Eduard Baranov, Simon Bliudze, Mohamad Jaber and Joseph Sifakis. A General Framework for Architecture Composability |
|
|
Domenico Bianculli, Carlo Ghezzi and Srdjan Krstic. Trace checking of Metric Temporal Logic with Aggregating Modalities using MapReduce |
|
| 18:00-20:00 | Welcome Reception at Le Canberra (on Campus, next to conference location) |
| September 4, 2014 (Thursday) | |
| 09:00 – 10:00 | Invited speaker : Joost-Pieter Katoen Model Checking Gigantic Markov Models Session Chair: Hubert Garavel |
| 10:00 – 10:30 | Coffee break |
| 10:30 – 12:30 | Session 4 – Real-Time and Embedded Systems |
| Session Chair: Martin Steffen | |
|
Jon Grov and Peter Olveczky. Megastore-CGC: Extending Megastore Using Formal Methods |
|
|
Reza Hajisheykhi, Ali Ebnenasir and Sandeep Kulkarni. Evaluating the Effect of Faults in SystemC TLM Models using UPPAAL |
|
|
Robert Reicherdt and Sabine Glesner. Formal Verification of Discrete-Time MATLAB/Simulink Models using Boogie |
|
|
Klaus Becker, Bernhard Schaetz, Michael Armbruster and Christian Buckl. A Formal Model for Constraint-Based Deployment Calculation and Analysis for Fault-Tolerant Systems |
|
| 12:30 – 14:00 | Lunch |
| 14:00 – 15:30 | Session 5 – Model Checking and Automata Learning |
| Session Chair: Radu Mateescu | |
|
Ivaylo Dobrikov and Michael Leuschel. Optimising the ProB Model Checker for B using Partial Order Reduction |
|
|
Alexandre Mota, Adalberto Farias, Andre Didier and Jim Woodcock. Rapid Prototying of a Semantically Correct Circus Model Checker |
|
|
Sofia Cassel, Falk Howar, Bengt Jonsson and Bernhard Steffen. An active learning algorithm for extended finite state machines |
|
| 15:30 – 16:00 | Coffee break |
| 16:30 – 18:30 | Guided Visit of Grenoble, meeting point: 16:30 at Office du Tourisme (between “Sainte claire les halles” and “Hubert Dubedout” tram stops on the B line, see map) |
| 19:30 | Banquet Dinner at Le Téléférique, restaurant on the Bastille top |
| September 5, 2014 (Friday) | |
| 09:00 – 10:00 | Invited speaker : Patrice Godefroid 500 Machine-Years of Software Model Checking and SMT Solving Session Chair: Dimitra Giannakopoulou |
| 10:00 – 10:30 | Coffee break |
| 10:30 – 12:30 | Session 6 – Tool Papers |
| Session Chair: Radu Calinescu | |
|
Qi Wang and Tim Wahls. Translating Event-B Machines to Database Applications |
|
|
Guillaume Brat, Jorge Navas, Nija Shi and Arnaud Venet. IKOS: a Framework for Static Analysis based on Abstract Interpretation |
|
|
Stefan Korecko, Ján Sorád, Zuzana Dudláková and Branislav Sobota. A Toolset for Support of Teaching Formal Software Development |
|
|
Ricardo J. Rodríguez, Lars-Ake Fredlund, Ángel Herranz and Julio Mariño. Execution and Verification of UML Diagrams with Erlang |
|
|
Diagne Fama, Amel Mammar and Marc Frappier. A Tool for Verifying Dynamic Properties in B |
|
|
David Hauzar and Jan Kofron. WeVerca: Web Applications Verification for PHP |
|
| 12:30 – 14:00 | Lunch |
| 14:00 – 15:30 | Session 7 – Program Correctness |
| Session Chair: Domenico Bianculli | |
|
Stefan Huster, Patrick Heckeler, Hanno Eichelberger, Jürgen Ruf, Sebastian Burg, Thomas Kropf and Wolfgang Rosenstiel. More Flexible Object Invariants With Less Specification Overhead |
|
|
Catherine Dubois and Renaud Rioboo. Verified Functional Iterators Using the FoCaLiZe Environment |
|
|
Tadeusz Sznuk and Aleksy Schubert. Tool support for teaching Hoare logic |
|
| 15:30 – 16:00 | Coffee break |
| 16:00 – 17:30 | Session 8 – Adaptive and Multi-Agent Systems |
| Session Chair: Bernhard Rumpe | |
|
Pierpaolo Degano, Gianluigi Ferrari and Letterio Galletta. A Two-Phase Static Analysis for Reliable Adaptation |
|
|
Linas Laibinis, Elena Troubitsyna, Zeineb Graja, Frederic Migeon and Ahmed Hadj Kacem. Formal Modelling and Verification of Cooperative Ant Behaviour in Event-B |
|
|
Raúl Pardo and Gerardo Schneider. A Formal Privacy Policy Framework for Social Networks |
|
| 17:30 – 17:45 | Closing (SEFM 2015, best paper award) |
PARTNERS
 |
 |
 |
 |
 |
 |
 |
