Wednesday, June 27

09:00 – 10:30

ECMFA Keynote 2

The future of modelling tools

(Mélanie Bats)

10:30 – 11:00 Coffee Break
11:00 – 12:30

Specification (Chair: Ina Schaeffer)

  • From Software Specifications to Constraint Programming

    (Stefan Hallerstede, Miran Hasanagić, Sebastian Krings, Peter Gorm Larsen, and Michael Leuschel)

  • Automated Specification Extraction and Analysis with Specstractor

    (Christoph Schulze, Rance Cleaveland, and Mikael Lindvall)

  • Bridging the Gap Between Informal Requirements and Formal Specifications Using Model Federation

    (Fahad Rafique Golra, Fabien Dagnat, Jeanine Souquières, Imen Sayar, and Sylvain Guerin)

12:30 – 14:00 Lunch Break
14:00 – 15:30

TAP Keynote



15:30 – 16:00 Coffee Break
16:00 – 17:30

Concurrency (Chair: Gwen Salün)

  • Program Verification for Exception Handling on Active Objects Using Futures

    (Crystal Chang Din, Rudolf Schlatte, and Tzu-Chun Chen)

  • Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems

    (Stefan Schupp and Erika Ábrahám)

  • FASTLANE Is Opaque – a Case Study in Mechanized Proofs of Opacity

    (Gerhard Schellhorn, Monika Wedel, Oleg Travkin, Jürgen König, and Heike Wehrheim)

Thursday, June 28

09:00 – 10:30

SEFM Keynote 1 (Chair: Einar Broch Johnsen)

We Need a Formal Semantics for Testability Transformation; SEFM community to the rescue?

(Mark Harman)

10:30 – 11:00 Coffee Break
11:00 – 12:30

Program Analysis (Chair: Heike Wehrheim)

  • Monte Carlo Tree Search for Finding Costly Paths in Programs

    (Kasper Luckow, Corina S. Păsăreanu, and Willem Visser)

  • A Cloud-Based Execution Framework for Program Analysis

    (Daniel Balasubramanian, Dmitriy Kostyuchenko, Kasper Luckow, Rody Kersten, and Gabor Karsai)

  • Cross-Architecture Lifter Synthesis

    (Rijnard van Tonder and Claire Le Goues)

12:30 – 14:00 Lunch Break
14:00 – 17:30 Social Event (AeroScopia Museum and Airbus Plant)
From 17:30 Gala dinner

Friday, June 29

09:00 – 10:30

SEFM Keynote 2 (Chair: Einar Broch Johnsen)

Hunting Resource Manipulation Bugs in Linux Kernel Code

(Andrzej Wasowski)

10:30 – 11:00 Coffee Break
11:00 – 12:30

Model Checking and Runtime Verification (Chair: Crystal Chang Din)

  • Counterexample Simplification for Liveness Property Violation

    (Gianluca Barbon, Vincent Leroy, and Gwen Salaün)

  • Online Enumeration of All Minimal Inductive Validity Cores

    (Jaroslav Bendík, Elaheh Ghassabani, Michael Whalen, and Ivana Černá)

  • Graph-Based Shape Analysis Beyond Context-Freeness

    (Hannah Arndt, Christina Jansen, Christoph Matheja, and Thomas Noll)

12:30 – 14:00 Lunch Break
14:00 – 15:30

Applications (Chair: Rance Cleaveland)

  • Formal Verification of Platoon Control Strategies

    (Adnan Rashid, Umair Siddique, and Osman Hasan)

  • Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover

    (Catherine Dubois, Olga Grinchtein, Justin Pearson, and Mats Carlsson)

  • Automated Validation of IoT Device Control Programs Through Domain-Specific Model Generation

    (Yunja Choi)

15:30 – 16:00 Coffee Break
16:00 – 17:30

Shape Analysis and Reuse (Chair: Marc Pantel)

  • Prevent: A Predictive Run-Time Verification Framework Using Statistical Learning

    (Reza Babaee, Arie Gurfinkel, and Sebastian Fischmeister)

  • Facilitating Component Reusability in Embedded Systems with GPUs

    (Gabriel Campeanu)