Past ARCH workshops

Program ARCH 2022 (September 06, 2022)

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)

14:00 Goran Frehse: Welcome Address
14:15 Mostafa Ayesh, Namya Mehan, Ethan Dhanraj, Abdul El-Rahwan, Simon Emil Opalka, Tony Fan, Akil Hamilton, Akshay Mathews Jacob, Rahul Anthony Sundarrajan, Bryan Widjaja and Claudio Menghi: Two Simulink Models with Requirements for a Simple Controller of a Pacemaker Device
14:30 Matthias Althoff: Benchmarks for the Formal Verification of Power Systems
14:45 Victor Gassmann and Matthias Althoff: Implementation of Ellipsoidal Operations in CORA 2022

15:00-15:30 (CEST) Coffee Break

15:30-17:00 (CEST) Results of the ARCH Friendly Competition

15:30 Piecewise Constant Dynamics (lead: Lei Bu)
15:40 Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
15:50 Nonlinear Systems (lead: Luca Geretti)
16:00 Stochastic Models (lead: Alessandro Abate)
16:10 Falsification (lead: Gidon Ernst)
16:20 Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)
16:30 Hybrid Programs (lead: Stefan Mitsch)
16.40 Voting for ARCH 2022 Best Result Award
16.50 Discussion on the future of the friendly competition

Program ARCH 2021 (July 09, 2021)

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)

16:30 Zahra Ramezani, Alexandre Donze, Martin Fabian and Knut Akesson: Temporal Logic Falsification of Cyber-Physical Systems using Input Pulse Generators
16:45 Niklas Kochdumper, Philipp Gassert and Matthias Althoff: Verification of Collision Avoidance for CommonRoad Traffic Scenarios
17:00 Jawher Jerray: ORBITADOR: A tool to analyze the stability of periodical dynamical systems
17:15 Matthias Althoff: Guaranteed State Estimation in CORA 2021

17:30-18:30 (CEST) Plenary Talk of Paulo Tabuada

18:30-19:30 (CEST) Results of the ARCH Friendly Competition

18:30 Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
18:40 Nonlinear Systems (lead: Luca Geretti)
18:50 Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)
19:00 Stochastic Models (lead: Alessandro Abate)
19:10 Falsification (lead: Gidon Ernst)
19:20 Hybrid Programs (lead: Stefan Mitsch)

19:30-19:35 (CEST) Break

19:35 Voting for ARCH 2021 Best Result Award
19:40 Discussion on the future of the friendly competition

Program ARCH 2020 (July 12, 2020)

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)

17:00 Jawher Jerray, Laurent Fribourg and Étienne André: Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method
17:15 Johan Lidén Eddeland, Sajed Miremadi and Knut Åkesson: Evaluating Optimization Solvers and Robust Semantics for Simulation-Based Falsification
17:30 Johan Lidén Eddeland, Alexandre Donzé, Sajed Miremadi and Knut Åkesson: Industrial Temporal Logic Specifications for Falsification of Cyber-Physical Systems
17:45 Maximilian Gaukler: Analysis of Real-Time Control Systems using First-Order Continuization
18:00 Ian Mitchell: A Robust Controlled Backward Reach Tube with (Almost) Analytic Solution for Two Dubins Cars
18:15 Edward Kim and Parasara Sridhar Duggirala: Kaa: A Python Implementation of Reachable Set Computation Using Bernstein Polynomials

18:30-18:45 (CEST) Break

18:45 Taylor Johnson: Tour through our online repository

19:00-20:10 (CEST) Results of the ARCH Friendly Competition

19:00 Piecewise Constant Dynamics plus BMC (lead: Lei Bu)
19:10 Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
19:20 Nonlinear Systems (lead: Luca Geretti)
19:30 Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)
19:40 Stochastic Models (lead: Alessandro Abate)
19:50 Falsification (lead: Gidon Ernst)
20:00 Hybrid Programs (lead: Stefan Mitsch)

20:10-20:15 (CEST) Break

20:15 Discussion on the future of the friendly competition

Program ARCH 2019 (April 15, 2019)

07:00-08:30 Registration

8:30 Invited Talk I: Nathalie Cauchi - Tools for Stochastic Hybrid Systems Quo Vadis

09:30-10:00 Results of the ARCH Friendly Competition I

09:30 Piecewise Constant Dynamics (lead: Goran Frehse)
09:40 Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
09:50 Nonlinear Dynamics (lead: Fabian Immler)

10:00-10:30 Coffee Break
10:30-12:00 Results of the ARCH Friendly Competition II and Contributed Papers

10:30 Stochastic Models (lead: Alessandro Abate)
10:40 Bounded Model Checking (lead: Lei Bu)
10:50 Falsification (lead: Gidon Ernst)
11:00 Hybrid Programs (lead: Stefan Mitsch)
11:10 AI category (lead: Taylor Johnson)
11:20 Sophie Gruenbacher, Jacek Cyranka, Md Ariful Islam, Max Tschaikowski, Scott Smolka and Radu Grosu: Under the Hood of a Stand-Alone Lagrangian Reachability Tool
11:40 Stanley Bak and Kerianne Hobbs: Efficient n-to-n Collision Detection for Space Debris using 4D AABB Trees

12:00-13:30 Lunch
13:30-15:00 Invited Talk II, Benckmark Proposals, and Discussion on Benchmark Formats

13:30 Invited Talk II: Taylor Johnson - Verification for Autonomous Cyber-Physical Systems with Machine Learning Components
14:30 Maximilian Gaukler and Peter Ulbrich: Worst-Case Analysis of Digital Control Loops with Uncertain Input/Output Timing (benchmark proposal)
14:40 Diego Manzanas Lopez, Patrick Musau, Hoang Dung Tran and Taylor T Johnson: Verification of Closed-loop Systems with Neural Network Controllers (benchmark proposal)
14:50 Discussion on Benchmark Formats

15:30-16:00 Coffe Break

16:00 Discussion on Repeatability Evaluation

Program ARCH 2018 (July 13, 2018)

09:00-10:00 Invited Talk

9:00 Erika Abraham - Old-established methods in a new look: How HyPro speeds up reachability computations for hybrid systems

0:50-12:00 Results of the ARCH friendly competition

10:50 Piecewise Constant Dynamics (lead: Goran Frehse)
11:00 Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
11:10 Nonlinear Dynamics (lead: Fabian Immler)
11:20 Stochastic Models (lead: Alessandro Abate)
11:30 Bounded Model Checking (lead: Lei Bu)
11:40 Falsification (lead: Georgios Fainekos)
11:50 Hybrid Programs (lead: Stefan Mitsch)

12:00-14:00 Lunch
14:00-15:10 Tools and Benchmarks I

14:00 Stanley Bak:
Verifying 10000-dimensional Linear Systems 10000x Faster
14:20 Matthias Althoff, Dmitry Grebenyuk and Niklas Kochdumper:
Implementation of Taylor models in CORA 2018
14:40 Peter Heidlauf, Alexander Collins, Michael Bolender and Stanley Bak:
Verification Challenges in F-16 Ground Collision Avoidance and Other Automated Maneuvers
14:55 Kerianne Hobbs, Peter Heidlauf, Alexander Collins and Stanley Bak:
Space Debris Collision Detection using Reachability

15:10-15:45 Coffee break
15:45-17:00 Benchmarks II

15:45 Patrick Musau and Taylor T Johnson:
Benchmark: Continuous-Time Recurrent Neural Networks
16:00 Patrick Musau, Diego Manzanas Lopez, Hoang Dung Tran and Taylor T Johnson:
Differential Algebraic Equations (DAEs) with Varying Index
16:15 Hoang Dung Tran, Tianshu Bao and Taylor T. Johnson:
Discrete-Space Analysis of Partial Differential Equations
16:30 Nikolaos Kekatos, Daniel Hess and Goran Frehse:
Lane change maneuver for autonomous vehicles
16:45 Nathalie Cauchi and Alessandro Abate:
A modular library of stochastic models from building automation systems

Program ARCH 2017 (April 17, 2017)

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

09:00 Invited Talk: Sebastian Scherer
Challenges for Safe Autonomous Flight
10:00 Daniele Ioli, Alessandro Falsone, Marianne Hartung, Axel Busboom and Maria Prandini:
A smart-grid energy management problem for data-driven design with probabilistic reachability guarantees
10:15 Nicole Chan and Sayan Mitra:
Verifying safety of an autonomous spacecraft rendezvous mission

10:30-11:00 Coffee break
11:00-12:00 Benchmarks II

11:00 Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang and Taylor Johnson:
Distributed Autonomous Systems
11:15 Alena Rodionova, Matthew O'Kelly, Houssam Abbas, Vincent Pacelli and Rahul Mangharam:
An Autonomous Vehicle Control Stack
11:30 Omar Beg, Ali Davoudi and Taylor T Johnson:
Reachability Analysis of Transformer-Isolated DC-DC Converters
11:45 Andreas Muller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and Andre Platzer:
A Benchmark for Component-based Hybrid Systems Safety Verification

12:00-13:30 Lunch
13:30-14:50 Contributed Papers

13:30 Xin Chen, Souradeep Dutta and Sriram Sankaranarayanan:
Formal Verification of a Multi-Basal Insulin Infusion Control Model
13:50 Christof Budnik, Sebastian Eckl and Marco Gario:
A Hybrid Testbed for Verification of Cyber-physical Production Systems
14:10 Nikolaos Kekatos, Marcelo Forets and Goran Frehse:
Modeling the Wind Turbine Benchmark with PWA Hybrid Automata
14:30 Stanley Bak and Parasara Sridhar Duggirala:
Direct Verification of Linear Systems with over 10000 Dimensions

14:50-15:30 Coffee break
15:30-17:00 ARCH Competition Results and Discussion

15:30 Affine and piecewise affine dynamics (lead: Matthias Althoff)
15:45 Nonlinear dynamics (lead: Xin Chen)
16:00 Piecewise constant dynamics (lead: Goran Frehse)
16:15 Bounded model checking (lead: Lei Bu)
16:30 Falsification and parameter-centric problems (lead: Georgios Fainekos)

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

Program ARCH 2016 (April 11, 2016)

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

Program ARCH 2015 (April 13, 2015)

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

Program ARCH 2014 (April 14, 2014)

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.