| Chair | 8:45-9:15 | Welcome 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:00 | Coffee 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:00 | Lunch 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:00 | Coffee 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 |
| Chair | ||
|---|---|---|
| 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:30 | Coffee 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:00 | Lunch 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:00 | Coffee 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:00 | Conference Banquet |
| Chair | ||
|---|---|---|
| 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:30 | Coffee 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:00 | Lunch 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:15 | Closing Remarks |
| 9:30-10:00 | Coffee 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/BSafe.network) |
|
| 12:00-13:30 | Lunch | 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 |