Program

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)

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

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