Friday, September 29

Chair8:45-9:15Welcome and Registration
9:15-9:30 Welcome
Patricia Derler, Klaus Schneider
Jean-Pierre Talpin 9:30-10:30 Keynote I: The Quest for Average Response Time
Thomas Henzinger, IST Austria (abstract and slides)
10:30-11:00Coffee Break
Sudipta Chattopadhyay 11:00-11:30 Stochastic Contracts for Cyber-Physical System Design Under Probabilistic Requirements
Jiwei Li, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Yugeng Xi and Dewei Li
11:30-12:00 On Improving Rare Event Simulation for Probabilistic Safety Analysis
Tim Gonschorek, Frank Ortmeier and Ben Lukas Rabeler
12:00-13:00Lunch Break
Jyotirmoy Deshmukh 13:00-13:30 Quantifying the Information Leak in Cache Attacks via Symbolic Execution
Sudipta Chattopadhyay, Moritz Beck, Ahmed Rezine and Andreas Zeller
13:30-14:00 Efficient Realization of Logical Execution Times in Legacy Embedded Software
Stefan Resmerita, Andreas Naderlinger and Stefan Lukesch
14:00-14:30 Model-Based Availability Analysis for Automated Production Systems: A Case Study
Jakob Mund, Maximilian Junker, Safa Bougouffa, Suhyun Cha and Birgit Vogel-Heuser
14:30-15:00Coffee Break
Pierluigi Nuzzo 15:00-15:30 Model-based, mutation-driven test case generation via heuristic-guided branching search
Andreas Fellner, Willibald Krenn, Thorsten Tarrach, Georg Weissenbacher and Rupert Schlick
15:30-16:00 Automatic Evaluation of Complex Design Decisions in Component-based Software Architectures
Max Scheerer, Axel Busch and Anne Koziolek
16:00-16:30 More than true or false: Native Support of Irregular Values in the Automatic Validation & Verification of UML/OCL Models
Nils Przigoda, Philipp Niemann, Judith Peters, Frank Hilken, Robert Wille and Rolf Drechsler
16:30-17:00 Property Templates for Checking Source Code Security
Elizabeth Leonard, Myla Archer and Constance Heitmeyer

Saturday, September 30

Patricia Derler 9:00-10:00 Keynote II: Formal Verification and Control Synthesis of Complex Dynamic Systems: Model-Based and Data-Driven Methods
Alessandro Abate (abstract and slides)
10:00-10:30Coffee Break
Georg Weissenbacher 10:30-11:00 Extraction of Missing Formal Assumptions in Under-Constrained Designs
Guillaume Plassan, Katell Morin-Allory and Dominique Borrione
11:00-11:30 Hyperproperties of Real-Valued Signals
Luan Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh and Taylor T Johnson
11:30-12:00 Yise - A novel Framework for Boolean Networks using Y-Inverter Graphs
Arun Chandrasekharan, Daniel Grosse and Rolf Drechsler
12:00-13:00Lunch Break
Mamoun Filali Amine 13:00-13:30 Using the Coq theorem prover to verify complex data structure invariants
Kenneth Roe and Scott Smith
13:30-14:00 A Core Calculus for Secure Hardware: Its Formal Semantics and Proof System
Thomas Reynolds, Adam Procter, William Harrison and Gerard Allwein
14:00-14:30 Releasing VDM Proof Obligations with SMT Solvers
Hsin-Hung Lin and Bow-Yaw Wang
14:30-15:00Coffee Break
Elizabeth Leonard 15:00-15:30 Simulation of Cyber-physical systems using IEC61499
Hammond Pearce, Matthew Kuo, Nathan Allen, Partha Roop and Avinash Malik
15:30-16:00 Monitoring Mobile and Spatially Distributed Cyber-Physical Systems
Ezio Bartocci, Luca Bortolussi, Michele Loreti and Laura Nenzi
19:00-22:00Conference Banquet

Sunday, October 1st

Klaus Schneider 9:00-10:00 Keynote III: Elevate embedded real-time programming with a synchronous language
Franz-Josef Grosch, Bosch GmbH (abstract and slides)
10:00-10:30Coffee Break
Stephen Edwards 10:30-11:00 Concurrent Execution System for Action Languages
Antti Jäskeläinen, Hannu-Matti Järvinen and Mikko Tiusanen
11:00-11:30 A Reactive Specification Formalism for Enhancing System Development, Analysis and Adaptivity
Assaf Marron
11:30-12:00 A Refinement-based compiler development for synchronous languages
Jean-Paul Bodeveix, Mamoun Filali-Amine and Kan Shuanglong
12:00-13:00Lunch Break
Klaus Schneider 13:00-13:30 Compositional Dataflow Circuits
Stephen A. Edwards, Richard Townsend and Martha A. Kim
13:30-14:00 Liam: An Elastic Programming Model
Haven Skinner, Rafael Possignolo and Jose Renau
14:00-15:00 Poster Session
15:00-15:15Closing Remarks

Monday, October 2nd - Joint Tutorials with FMCAD

9:30-10:00Coffee and Registration
10:00-12:00 How Formal Methods and Analysis Helps Security of Entire Blockchain-based Systems
Shin'ichiro Matsuo (Georgetown University/CELLOS Consortium/
13:30-15:30 Symbolic Security Analysis using the Tamarin Prover
Cas Cremers, Oxford University
15:30-16:00 Coffee
16:00-18:00 Consistency properties of parallel/distributed programs in cat
Jade Alglave, University College London / Microsoft Research