Benchmarks

Benchmark proposals presented at ARCH, with papers and model files.

Benchmarks 2020

Title	Authors	Attachments
A Robust Controlled Backward Reach Tube with (Almost) Analytic Solution for Two Dubins Cars	Ian Mitchell	attachment
Industrial Temporal Logic Specifications for Falsification of Cyber-Physical Systems	Johan Liden Eddeland, Alexandre Donze, Sajed Miremadi and Knut Akesson	attachment

Benchmarks 2019

Title	Authors	Attachments
Worst-Case Analysis of Digital Control Loops with Uncertain Input/Output Timing	Maximilian Gaukler and Peter Ulbrich	attachment
Verification of Closed-loop Systems with Neural Network Controllers	Diego Manzanas Lopez, Patrick Musau, Hoang-Dung Tran and Taylor T. Johnson	attachment

Benchmarks 2018

Title	Authors	Attachments
Linear Differential-Algebraic Equations	Patrick Musau, Diego Manzanas Lopez, Hoang-Dung Tran and Taylor T. Johnson	attachment
Discrete-Space Analysis of Partial Differential Equations	Hoang-Dung Tran, Tianshu Bao and Taylor T. Johnson	attachment
Verification of Continuous Time Recurrent Neural Networks	Patrick Musau and Taylor T. Johnson	attachment
Verification Challenges in F-16 Ground Collision Avoidance and Other Automated Maneuvers	Peter Heidlauf, Alexander Collins, Michael Bolender and Stanley Bak	attachment
Space Debris Collision Detection using Reachability	Kerianne Hobbs, Peter Heidlauf, Alexander Collins and Stanley Bak	attachment
Lane change maneuver for autonomous vehicles	Nikolaos Kekatos, Daniel Hess and Goran Frehse	attachment
Benchmarks for stochastic models from building automation systems	Nathalie Cauchi and Alessandro Abate	attachment

Benchmarks 2017

Title	Authors	Attachments
A Smart-Grid Energy Management Problem for Data-Driven Design with Probabilistic Reachability Guarantees	Daniele Ioli, Alessandro Falsone, Marianne Hartung, Axel Busboom and Maria Prandini	attachment
A Benchmark for Component-based Hybrid Systems Safety Verification	Andreas Muller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and Andre Platzer	attachment
Reachability Analysis of Transformer-Isolated DC-DC Converters	Omar Beg, Ali Davoudi and Taylor T Johnson	attachment
An Autonomous Vehicle Control Stack	Alena Rodionova, Matthew O'Kelly, Houssam Abbas, Vincent Pacelli and Rahul Mangharam	attachment
Distributed Autonomous Systems	Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang and Taylor Johnson	-
Verifying Safety of an Autonomous Spacecraft Rendezvous Mission	Nicole Chan and Sayan Mitra	attachment

Benchmarks 2016

Title	Authors	Attachments
Nonlinear Hybrid Automata Model of Excitable Cardiac Tissue	Houssam Abbas, Kuk Jin Jang and Rahul Mangharam	attachment
Hybrid automata model of the heart for formal verification of pacemakers	Sidharta Andalam, Avinash Malik, Partha Roop and Mark Trew	attachment
Chains of Integrators as a Benchmark for Scalability of Hybrid Control Synthesis	Scott Livingston and Vasumathi Raman	attachment
Benchmarks for Non-linear Continuous System Safety Verification	Andrew Sogokon, Taylor T Johnson and Khalil Ghorbal	attachment
Formal Verification of Charge Pump Phase-Locked Loop and Full Wave Rectifier Through Reachability Analysis	Omar Beg, Ali Davoudi and Taylor T Johnson	attachment
Hybrid modelling of a wind turbine	Simone Schuler, Fabiano Daher Adegas and Adolfo Anta	attachment
Benchmark for Verification of Fault-Tolerant Clock Synchronization Algorithms	Sergiy Bogomolov, Christian Herrera and Wilfried Steiner	attachment
Large-Scale Linear Systems from Order-Reduction	Hoang-Dung Tran, Luan Viet Nguyen and Taylor T Johnson	attachmentUpdate_27Mar2017 attachment

Benchmarks 2015

Title	Authors	Attachments
Benchmark problem: an air brake model for trains	Luca Parolini, Simone Schuler, Adolfo Anta	attachment
Benchmark: Quadrotor Attitude Control	Antonio Eduardo Carrilho da Cunha	attachment
Benchmark: Stratified Controllers of Tank Networks	Stanley Bak, Sergiy Bogomolov, Marius Greitschus, Taylor T. Johnson	attachment
Benchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis	Hoang-Dung Tran, Luan Viet Nguyen, Taylor T. Johnson	attachment

Benchmarks 2014

Title	Authors	Attachments
Reachability on a model with holes	Thomas Heinz, Jens Oehlerking, Matthias Woehrle	attachment
Benchmarks for Model Transformations and Conformance Checking	Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts	attachmentUpdate_18Dec2014 attachment
Motor-Transmission Drive System: a Benchmark Example for Safety Verification	Hongxu Chen, Sayan Mitra, and Guangyu Tian	attachmentUpdate_06April2017 attachment SimulinkUpdate_06Apr2017 Simulink
A PK/PD Model and Safety Constraints for Anesthesia Delivery	Victor Gan, Guy A. Dumont and Ian M. Mitchell	attachment
DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters)	Luan Viet Nguyen and Taylor T. Johnson	attachment
Flight Envelope Protection in Autonomous Quadrotors	Shahab Kaynama and Claire J. Tomlin	attachment
Networked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools	Ibtissem Ben Makhlouf and Stefan Kowalewski	attachment
Benchmarks for Temporal Logic Requirements for Automotive Systems	Bardh Hoxha, Houssam Abbas, Georgios Fainekos