Program

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

Logo Inria Logo Grenoble INP Logo LIG Logo CNRS Logo UJF
Logo RMIT Logo LaMetro