Archive
Past ARCH workshops
- 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)
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.