Past ARCH workshops

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.