Past ARCH workshops

Program ARCH 2023 (May 09, 2023)

08:00 - 09:00

Breakfast/Continental

Zoom Link: https://zoom.us/j/97903297749

09:00 - 10:00Contributed Papers (12 min presentation, 8 min discussion)
09:00Goran Frehse: Welcome Address
09:20Sanaz Sheikhi and Stanley Bak: Closed-Loop ACAS Xu Neural Network Verification (Benchmark Proposal)
09:40Matthias Althoff: Checking and Establishing Reachset Conformance in CORA 2023
10:00 - 10:30 Coffee Break
10:30 - 12:00 Results of the ARCH Friendly Competition
10:30Piecewise Constant Dynamics (lead: Lei Bu)
10:40Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
10:50Nonlinear Systems (lead: Luca Geretti)
11:00Stochastic Models (lead: Alessandro Abate)
11:10Falsification (lead: Gidon Ernst)
11:20Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)
11:30Hybrid Programs (lead: Stefan Mitsch)
11:40Voting for ARCH 2023 Best Result Award

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:00Goran Frehse: Welcome Address
14:15Mostafa 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:30Matthias Althoff: Benchmarks for the Formal Verification of Power Systems
14:45Victor 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:30Piecewise Constant Dynamics (lead: Lei Bu)
15:40Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
15:50Nonlinear Systems (lead: Luca Geretti)
16:00Stochastic Models (lead: Alessandro Abate)
16:10Falsification (lead: Gidon Ernst)
16:20Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)
16:30Hybrid Programs (lead: Stefan Mitsch)
16.40Voting for ARCH 2022 Best Result Award
16.50Discussion 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:30Zahra Ramezani, Alexandre Donze, Martin Fabian and Knut Akesson: Temporal Logic Falsification of Cyber-Physical Systems using Input Pulse Generators
16:45Niklas Kochdumper, Philipp Gassert and Matthias Althoff: Verification of Collision Avoidance for CommonRoad Traffic Scenarios
17:00Jawher Jerray: ORBITADOR: A tool to analyze the stability of periodical dynamical systems
17:15Matthias 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:30Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
18:40Nonlinear Systems (lead: Luca Geretti)
18:50Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)
19:00Stochastic Models (lead: Alessandro Abate)
19:10Falsification (lead: Gidon Ernst)
19:20Hybrid Programs (lead: Stefan Mitsch)
19:30-19:35 (CEST) Break
19:35Voting for ARCH 2021 Best Result Award
19:40Discussion 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:00Jawher Jerray, Laurent Fribourg and Étienne André: Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method
17:15Johan Lidén Eddeland, Sajed Miremadi and Knut Åkesson: Evaluating Optimization Solvers and Robust Semantics for Simulation-Based Falsification
17:30Johan Lidén Eddeland, Alexandre Donzé, Sajed Miremadi and Knut Åkesson: Industrial Temporal Logic Specifications for Falsification of Cyber-Physical Systems
17:45Maximilian Gaukler: Analysis of Real-Time Control Systems using First-Order Continuization
18:00Ian Mitchell: A Robust Controlled Backward Reach Tube with (Almost) Analytic Solution for Two Dubins Cars
18:15Edward Kim and Parasara Sridhar Duggirala: Kaa: A Python Implementation of Reachable Set Computation Using Bernstein Polynomials
18:30-18:45 (CEST) Break
18:45Taylor Johnson: Tour through our online repository
19:00-20:10 (CEST)Results of the ARCH Friendly Competition
19:00Piecewise Constant Dynamics plus BMC (lead: Lei Bu)
19:10Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
19:20Nonlinear Systems (lead: Luca Geretti)
19:30Artificial Intelligence and Neural Network Control Systems (lead: Taylor Johnson)
19:40Stochastic Models (lead: Alessandro Abate)
19:50Falsification (lead: Gidon Ernst)
20:00Hybrid Programs (lead: Stefan Mitsch)
20:10-20:15 (CEST) Break
20:15Discussion on the future of the friendly competition

Program ARCH 2019 (April 15, 2019)

07:00-08:30Registration
8:30Invited Talk I: Nathalie Cauchi - Tools for Stochastic Hybrid Systems Quo Vadis
09:30-10:00 Results of the ARCH Friendly Competition I
09:30Piecewise Constant Dynamics (lead: Goran Frehse)
09:40Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
09:50Nonlinear Dynamics (lead: Fabian Immler)
10:00-10:30 Coffee Break   
10:30-12:00Results of the ARCH Friendly Competition II and Contributed Papers
10:30Stochastic Models (lead: Alessandro Abate)
10:40Bounded Model Checking (lead: Lei Bu)
10:50Falsification (lead: Gidon Ernst)
11:00Hybrid Programs (lead: Stefan Mitsch)
11:10AI category (lead: Taylor Johnson)
11:20Sophie Gruenbacher, Jacek Cyranka, Md Ariful Islam, Max Tschaikowski, Scott Smolka and Radu Grosu: Under the Hood of a Stand-Alone Lagrangian Reachability Tool
11:40Stanley Bak and Kerianne Hobbs: Efficient n-to-n Collision Detection for Space Debris using 4D AABB Trees
12:00-13:30Lunch
13:30-15:00Invited Talk II, Benckmark Proposals, and Discussion on Benchmark Formats
13:30Invited Talk II: Taylor Johnson - Verification for Autonomous Cyber-Physical Systems with Machine Learning Components
14:30Maximilian Gaukler and Peter Ulbrich: Worst-Case Analysis of Digital Control Loops with Uncertain Input/Output Timing (benchmark proposal)
14:40Diego Manzanas Lopez, Patrick Musau, Hoang Dung Tran and Taylor T Johnson: Verification of Closed-loop Systems with Neural Network Controllers (benchmark proposal)
14:50Discussion on Benchmark Formats
15:30-16:00Coffee Break
16:00Discussion on Repeatability Evaluation

Program ARCH 2018 (July 13, 2018)

09:00-10:00 Invited Talk

9:00Erika Abraham - Old-established methods in a new look: How HyPro speeds up reachability computations for hybrid systems
10:50-12:00Results of the ARCH friendly competition
10:50Piecewise Constant Dynamics (lead: Goran Frehse)
11:00Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff)
11:10Nonlinear Dynamics (lead: Fabian Immler)
11:20Stochastic Models (lead: Alessandro Abate)
11:30Bounded Model Checking (lead: Lei Bu)
11:40Falsification (lead: Georgios Fainekos)
11:50Hybrid Programs (lead: Stefan Mitsch)
12:00-14:00 Lunch     
14:00-15:10Tools and Benchmarks I
14:00Stanley Bak:          
Verifying 10000-dimensional Linear Systems 10000x Faster
14:20Matthias Althoff, Dmitry Grebenyuk and Niklas Kochdumper:          
Implementation of Taylor models in CORA 2018
14:40Peter Heidlauf, Alexander Collins, Michael Bolender and Stanley Bak:          
Verification Challenges in F-16 Ground Collision Avoidance and Other Automated Maneuvers
14:55Kerianne Hobbs, Peter Heidlauf, Alexander Collins and Stanley Bak:          
Space Debris Collision Detection using Reachability
15:10-15:45 Coffee break 
15:45-17:00Benchmarks II
15:45Patrick Musau and Taylor T Johnson:          
Benchmark: Continuous-Time Recurrent Neural Networks
16:00Patrick Musau, Diego Manzanas Lopez, Hoang Dung Tran and Taylor T Johnson:          
Differential Algebraic Equations (DAEs) with Varying Index
16:15Hoang Dung Tran, Tianshu Bao and Taylor T. Johnson:          
Discrete-Space Analysis of Partial Differential Equations
16:30Nikolaos Kekatos, Daniel Hess and Goran Frehse:          
Lane change maneuver for autonomous vehicles
16:45Nathalie 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:00Invited Talk: Sebastian Scherer          
Challenges for Safe Autonomous Flight
10:00Daniele 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:15Nicole Chan and Sayan Mitra:          
Verifying safety of an autonomous spacecraft rendezvous mission
10:30-11:00 Coffee break     
11:00-12:00Benchmarks II
11:00Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang and Taylor Johnson:          
Distributed Autonomous Systems
11:15Alena Rodionova, Matthew O'Kelly, Houssam Abbas, Vincent Pacelli and Rahul Mangharam:          
An Autonomous Vehicle Control Stack
11:30Omar Beg, Ali Davoudi and Taylor T Johnson:          
Reachability Analysis of Transformer-Isolated DC-DC Converters
11:45Andreas 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:50Contributed Papers
13:30Xin Chen, Souradeep Dutta and Sriram Sankaranarayanan:          
Formal Verification of a Multi-Basal Insulin Infusion Control Model
13:50Christof Budnik, Sebastian Eckl and Marco Gario:          
A Hybrid Testbed for Verification of Cyber-physical Production Systems
14:10Nikolaos Kekatos, Marcelo Forets and Goran Frehse:          
Modeling the Wind Turbine Benchmark with PWA Hybrid Automata
14:30Stanley Bak and Parasara Sridhar Duggirala:          
Direct Verification of Linear Systems with over 10000 Dimensions
14:50-15:30 Coffee break 
15:30-17:00ARCH Competition Results and Discussion
15:30Affine and piecewise affine dynamics (lead: Matthias Althoff)
15:45Nonlinear dynamics (lead: Xin Chen)
16:00Piecewise constant dynamics (lead: Goran Frehse)
16:15Bounded model checking (lead: Lei Bu)
16:30Falsification 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.