Archive

Past ARCH workshops

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.