• 2023: 10th ARCH workshop in San Antonio, USA (call for submissions)
• 2022: 9th ARCH workshop in Munich, Germany (call for submissions)
• 2021: 8th ARCH (virtual) workshop in Brussels, Belgium (call for submissions)
• 2020: 7th ARCH (virtual) workshop in Berlin, Germany (call for submissions)
• 2019: 6th ARCH workshop in Montreal, Canada (call for submissions)
• 2018: 5th ARCH workshop in Oxford, UK (call for submissions)
• 2017: 4th ARCH workshop in Pittsburgh, USA (call for submission)
• 2016: 3rd ARCH workshop in Vienna, Austria (call for submissions)
• 2015: 2nd ARCH workshop in Seattle, USA (call for submissions)
• 2014: 1st ARCH workshop in Berlin, Germany (call for submissions)

Since we will have a hybrid event (remote and in-person participation), we shortened the program to accommodate as many time zones as possible. All workshops at SAFECOMP have to end before 17.00 so that participants can join the evening event in downtown Munich at 18.30.

12:30-13:30 (CEST) Lunch Break (Lunch is offered for all participants who have registered as on-site present)

14:00-15:00 (CEST) Contributed Papers (10 min presentation, 5 min discussion)

Since we will have a live online event, we shortened the program to accommodate as many time zones as possible. Recording of the workshop.

16:30-17:30 (CEST) Contributed Papers (10 min presentation, 5 min discussion)

Since this was a live and online workshop, we shortened the program to accomodate as many time zones as possible. Recordings of the workshop.

17:00-18:30 (CEST) Contributed Papers (tentative; 10 min presentation, 5 min discussion)

09:00-10:00 Invited Talk

09:00-10:30 Invited Talk and Benchmarks I

17:00-18:00 Tour through CMU Robotics Center

Pdf version of the program.

08:00 Registration          
09:00-10:25 Invited Talk and Benchmarks I

• Invited Talk: Dirk Beyer: Reliable and Reproducible Competition Results
• Houssam Abbas, Kuk Jin Jang and Rahul Mangharam:          
  Nonlinear Hybrid Automata Model of Excitable Cardiac Tissue
• Sidharta Andalam, Avinash Malik, Partha Roop and Mark Trew:          
  Hybrid automata model of the heart for formal verification of pacemakers

10:25-11:00 Coffee break          
11:00-12:20 Benchmarks II

• Scott Livingston and Vasumathi Raman:          
  Chains of Integrators as a Benchmark for Scalability of Hybrid Control Synthesis
• Andrew Sogokon, Taylor T Johnson and Khalil Ghorbal:          
  Benchmarks for Non-linear Continuous System Safety Verification
• Omar Beg, Ali Davoudi and Taylor T Johnson:          
  Formal Verification of Charge Pump Phase-Locked Loop and Full Wave Rectifier Through Reachability Analysis
• Simone Schuler, Fabiano Daher Adegas and Adolfo Anta:          
  Hybrid modelling of a wind turbine

12:20-14:00 Lunch          
14:00-15:20 Benchmarks III and Tools I

• Sergiy Bogomolov, Christian Herrera and Wilfried Steiner:          
  Benchmark for Verification of Fault-Tolerant Clock Synchronization Algorithms
• Hoang-Dung Tran, Luan Viet Nguyen and Taylor T Johnson:          
  Large-Scale Linear Systems from Order-Reduction
• Stanley Bak, Sergiy Bogomolov and Christian Schilling:          
  High-level Hybrid Systems Analysis with Hypy
• Ibtissem Ben Makhlouf, Norman Hansen and Stefan Kowalewski:          
  HyReach: A Reachability Tool for Linear Hybrid Systems Based on Support Functions

15:20-16:00 Coffee break          
16:00-17:20 Tools II

• Axel Busboom, Simone Schuler and Alexander Walsch:          
  FormalSpec - semi-automatic formalization of system requirements for formal verification
• Dalibor Drzajic, Nikolaos Kariotoglou, Maryam Kamgarpour and John Lygeros:          
  A Semidefinite Programming Approach to Control Synthesis for Stochastic Reach-Avoid Problems
• Heinz Riener, Robert Koenighofer, Goerschwin Fey and Roderick Bloem:          
  SMT-Based CPS Parameter Synthesis and Repair
• Matthias Althoff and Dmitry Grebenyuk          
  Implementation of Interval Arithmetic in CORA 2016

08:00 Registration          
08:30-10:00 Invited Talk & Tool Presentation

• Invited Talk: Jay Abraham (Mathworks) - Verification and test of embedded software with model-based design
• Chuchu Fan, Parasara Sridhar Duggirala, Sayan Mitra and Mahesh Viswanathan:          
  Progress on Powertrain Verification Challenge with C2E2

10:00-10:30 Coffee break          
10:30-12:00 Tools

• Matthias Althoff:          
  An Introduction to CORA 2015
• Fabian Immler:          
  Isabelle/HOL for Reachability Analysis of Continuous Systems
• Stefano Minopoli and Goran Frehse:          
  Running SpaceEx on the ARCH14 Benchmarks
• Xin Chen, Sriram Sankaranarayanan and Erika Abraham:          
  Flow* 1.2: More Effective to Play with Hybrid Systems

12:00-13:00 Lunch          
13:00-14:30 Tools & Experience Reports

• Alexandre Donze and Vasumathi Raman:          
  BluSTL: Controller Synthesis from Signal Temporal Logic Specifications
• Kyungmin Bae, Soonho Kong and Sicun Gao:          
  SMT Encoding of Hybrid Systems in dReal
• Thomas Strathmann and Jens Oehlerking:          
  Verifying Properties of an Electro-Mechanical Braking System
• Hendrik Roehm, Rainer Gmehlich, Thomas Heinz, Jens Oehlerking and Matthias Woehrle:          
  Industrial Examples of Formal Specifications for Test Case Generation

14:30-15:00 Coffee break          
15:00-17:00 Benchmarks

• Luca Parolini, Simone Schuler and Adolfo Anta:          
  An air brake model for trains
• Jyotirmoy Deshmukh, Hisahiro Ito, Xiaoqing Jin, James Kapinski, Ken Butts, Behzad Samadi and Kevin Walker:          
  PWA Models of a Powertrain Control Benchmark
• Hoang-Dung Tran, Luan Viet Nguyen and Taylor T Johnson:          
  A Nonlinear Reachability Analysis Test Set from Numerical Analysis
• A. E. C. Da Cunha:          
  Quadrotor Attitude Control
• Stanley Bak, Sergiy Bogomolov, Marius Greitschus and Taylor T Johnson:          
  Benchmark Generator for Stratified Controllers of Tank Networks

08:00 Registration          
09:00-11:00 Invited Talk and Benchmark Presentations I

• Invited Talk: Bernard Dion (Esterel Technologies) - 15 years of Industry experience in developing and verifying critical systems
• Victor Gan, Guy A. Dumont and Ian M. Mitchell. Benchmark Problem: A PK/PD Model and Safety Constraints for Anesthesia Delivery
• Hongxu Chen, Sayan Mitra and Guangyu Tian. Motor-Transmission Drive System: a Benchmark Example for Safety Verification
• Bardh Hoxha, Houssam Abbas and Georgios Fainekos. Benchmarks for Temporal Logic Requirements for Automotive Systems

11:00-11:30 Coffee break          
11:30-13:00 Benchmark Presentations II

• Thomas Heinz, Jens Oehlerking and Matthias Woehrle. Benchmark: Reachability on a model with holes
• Ibtissem Ben Makhlouf. WLAN Cooperative Platoon of Vehicles for Testing Methods and Verification Tools
• Luan Nguyen and Taylor T Johnson. Benchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters)
• Xiaoqing Jin, Jyotirmoy Deshmukh, James Kapinski, Koichi Ueda and Ken Butts. Benchmarks for Model Transformations and Conformance Checking

13:00-14:00 Lunch          
14:00-16:00 Experience Reports and Tool Presentations

• Olivier Bouissou, Alexandre Chapoutot and Samuel Mimram. Simulation and Verification of Hybrid Systems using HySon
• Eike Moehlmann, Willem Hagemann and Astrid Rakow. Verifying a PI Controller using SoapBox and Stabhyli
• Bardh Hoxha, Houssam Abbas and Georgios Fainekos. Using S-TaLiRo on Industrial Size Automotive Models

16:00-16:30 Coffee break          
16:30-18:00 Benchmark Repository and Panel Discussion

• Presentation and Discussion of the Online Benchmark Repository
• Panel Discussion: How to certify cyber-physical systems? Perspectives from industry and academia.