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) | |
iss | see paper (many tools) | see paper (many people) | ||
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 2020
Title | Authors | Attachments |
A Robust Controlled Backward Reach Tube with (Almost) Analytic Solution for Two Dubins Cars | Ian Mitchell | - |
Industrial Temporal Logic Specifications for Falsification of Cyber-Physical Systems | Johan Liden Eddeland, Alexandre Donze, Sajed Miremadi and Knut Akesson | - |
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
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