Benchmarks

Solved Benchmarks

Benchmark title Benchmark instance Tool(s) Solved by Reference
DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters) - SpaceEx Stefano Minopoli and Goran Frehse paper
Networked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools deterministic failure SpaceEx Stefano Minopoli and Goran Frehse paper
non-deterministic failure SpaceEx, CORA Goran Frehse, Matthias Althoff paper
arbitrary failure CORA Matthias Althoff paper
Benchmarks for Model Transformations and Conformance Checking model 3 C2E2 Chuchu Fan, Parasara Sridhar Duggirala, Sayan Mitra, and Mahesh Viswanathan paper
Large-Scale Linear Systems from Order-Reduction building see papers (many tools) see papers (many people)

paper1

paper2
iss see paper (many tools) see paper (many people)

paper
Benchmark: Quadrotor Attitude Control comment: controller added to make problem more interesting Flow*, CORA Xin Chen, Matthias Althof paper

Verifying safety of an autonomous spacecraft rendezvous mission

 linear see paper (many tools) see paper (many people) paper
nonlinear see paper (many tools) see paper (many people) paper

Benchmarks 2019

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

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 -
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 -
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 -
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