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