Tuesday, July 5

09:00 – 10:30

ICGT Keynote

Complexity is the Only Constant: Thoughts on Trends in Computing and Their Relevance to MDE

(Juergen Dingel)

10:30 – 11:00 Coffee Break

Opening by eva Kühn

11:00 – 12:45

Concurrency and Non-Interference (chair: Graeme Smith)

  • Automatic Derivation of Platform Noninterference Properties

    (Oliver Schwarz and Mads Dam)

  • Linearizability and Causality

    (Simon Doherty and John Derrick)

  • Refinement-based verification of Communicating Unstructured Code

    (Nils Jähnig, Thomas Göthel and Sabine Glesner)

  • Guided Dynamic Symbolic Execution Using Subgraph Control-Flow Information (short paper)

    (Josselin Feist, Mounier Laurent and Marie-Laure Potet)

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

TAP Keynote

From Testing and Verification to Performance Analysis and Synthesis of Cyber-Physical Systems

(Kim G. Larsen)

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

Program Analysis (chair: Alessandro Cimatti)

  • Correlating Structured Inputs and Outputs in Functional Specifications

    (Oana Fabiana Andreescu, Thomas Jensen and Stéphane Lescuyer)

  • Combining Predicate Abstraction with Fixpoint Approximations

    (Tuba Yavuz)

  • Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis

    (Jaroslav Bendík, Nikola Benes, Jiri Barnat and Ivana Cerna)

  • Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams

    (Christian Dernehl, Norman Hansen and Stefan Kowalewski)


Wednesday, July 6

09:00 – 10:30

Keynote (chair: Rocco De Nicola)

Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems

(Gul Agha)

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

Model Checking (chair: Antonio Cerone)

  • Program Generation using Simulated Annealing and Model Checking

    (Idress Husien and Sven Schewe)

  • LTL Parameter Synthesis of Parametric Timed Automata

    (Peter Bezděk, Nikola Beneš, Jiří Barnat and Ivana Černá)

  • Model checking simulation rules for linearizability

    (Graeme Smith)

  • LTL Model Checking under Fairness in ProB (short paper)

    (Ivaylo Dobrikov, Daniel Plagge and Michael Leuschel)

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

Keynote (chair: eva Kühn)

Satisfiability Checking: Theory and Applications

(Erika Ábrahám)

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

Verification (chair: Vesna Šešum-Čavić)

  • Counterexamples from Proof Failures in SPARK

    (David Hauzar, Claude Marché and Yannick Moy)

  • Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution

    (Jera Hensel, Jürgen Giesl, Florian Frohn and Thomas Ströder)

  • SMT-based automatic proof of ASM model refinement

    (Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene)

  • Coq Implementation of OO Verification Framework VeriJ (short paper)

    (Ke Zhang and Zongyan Qiu)

  • Towards a Proof Framework for Information Systems with Weak Consistency (short paper)

    (Peter Zeller and Arnd Poetzsch-Heffter)

18:00 – 18:05

SEFM 2017 Announcement by Alessandro Cimatti


Thursday, July 7

09:00 – 10:30

ECMFA Keynote

A Model-Based Driver’s License for Self-Driving Cars: Challenges and Future Directions

(Krzysztof Czarnecki)

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

Interaction and Adaptation (chair: Erika Ábrahám)

  • A Cognitive Framework based on Rewriting Logic for the Analysis of Interactive Systems

    (Antonio Cerone)

  • Incentive Stackelberg Mean-payoff Games

    (Anshul Gupta, Sven Schewe, Ashutosh Trivedi, Maram Sai Krishna Deepak and Bharath Kumar Padarthi)

  • Stability-based Adaptation of Asynchronously Communicating Software

    (Carlos Canal and Gwen Salaün)

  • Compliance Checking in the Open Payments Ecosystem (short paper)

    (Shaun Azzopardi, Christian Colombo, Gordon Pace and Brian Vella)

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

TAP Industrial Keynote

Using Formal Methods for Verification and Validation in Railway

(Klaus Reichl)

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

Development Methods (chair: Gwen Salaün)

  • CoCoSpec: A mode aware contract language

    (Adrien Champion, Arie Gurfinkel, Temesghen Kahsai and Cesare Tinelli)

  • Modularizing Crosscutting Concerns in Component-Based Systems

    (Antoine El-Hokayem, Ylies Falcone and Mohamad Jaber)

  • Tightening a Contract Refinement

    (Alessandro Cimatti, Ramiro Demasi and Stefano Tonetta)

  • BMotionWeb: A Tool for Rapid Creation of Formal Prototypes

    (Lukas Ladenberger and Michael Leuschel)

Closing by Rocco De Nicola