Benchmarks
This page contains links to Benchmarks studied in AVACS. Access to some of them is password protected. Those are marked with PP.
Benchmarks 2nd funding period
Name | Used in | PP | Description | Model |
Approach Velocity Controller | H3 | no | ||
Bouncing Balls | H4 | no | ||
Bounded Retransmission Protocol | S2 | no | ||
Bounded Retransmission Protocol | S3 | no | ||
Blackbox BMC Suite | S1, H1/2 | yes | ||
Chord Network | S3 | yes | ||
Contract Signing Protokoll | S3 | yes | ||
Crowds Protokoll | S3 | yes | ||
CSMACD | S2 | no | ||
Dam | H3 | no | ||
Dam (Extended) | H3 | yes | ||
Erlang Stages | S3 | no | ||
ETCS Emergency Messages | R1 | yes | ||
ETCS Example | H3 | yes | ||
ETCS Train System
| H1/2 | no | ||
Flap/Slat Benchmarks | H3 | no | ||
iSAT-LP Benchmarks | H1/2 | yes | ||
iSAT-Craig Benchmarks | H1/2 | yes | ||
iSAT-ODE Benchmarks | H1/2 | no | ||
iSAT Traffic Benchmarks | H1/2 | no | ||
Jackson Queues | S3 | no | ||
Lane Change Assistant | H3 | yes | ||
Lawn Mower | H4 | no | ||
Mastermind | S3 | no | n.a. | |
Moving Block Train Control | H4 | no | ||
Networked Automation System (for SiSAT) | H1/2 | yes | ||
Networked Control System | H1/2 | no | ||
Protein Synthesis | S3 | no | ||
Quasi-Birth-Death Processes | S3 | no | ||
Random Walk | S3 | no | ||
Randomized Consensus | S3 | no | ||
Randomized Mutual Exclusion | S3 | no | ||
Randomized Scheduling | S3 | no | n.a. | |
Railroad Crossing | H3 | no | ||
RBC Complex Topologies | R1 | no | ||
RCAS Example | H3 | yes | n.a. | |
Stoachastic Job Scheduling | S3 | no | ||
Synchronous Leader Election Protocol | S3 | yes | ||
SPASS(iSAT) Benchmarks | H1/2 | yes | ||
SPASS(Z3) Benchmarks | H1/2 | yes | ||
Self-stabilizing Minimal Spanning Tree | S3 | yes | ||
Tandem Queues | S3 | no | ||
Temperature Control | H4 | no | ||
Thermostat | H4 | no | ||
Timed Blackbox BMC Suite | S1 | yes | ||
Two Tank System (iSAT(ODE)) | H1/2 | yes | ||
ViDAS | R2 | yes | ||
Water Level Control | H4 | no | ||
Water Level Control (HSCC'11) | H4 | no | ||
Wireless LAN | S2 | no | ||
Workstation Cluster | S3 | no | ||
Zeroconf | S3 | no | ||
External | Link to | |||
Hardware Model Checking Competition benchmark set 2008 | H1/2 | |||
Hardware Model Checking Competition benchmark set 2010 | H1/2 | |||
H-PILoT | R1, H3 | External Link (Download) | ||
HSolver Benchmarks | H1/2 | |||
HySAT Benchmarks | H1/2 | |||
iSAT Benchmarks | H1/2 | |||
LIRA Benchmarks | H1/2 | Benchmark and simple dokumentation in GForge | ||
Mälardalen Benchmarks | R2 | |||
QBFLIB | S1 | |||
SAT Competition Benchmarks | H1/2 | |||
SMT-LIB | H1/2, R1 | |||
Benchmarks 1st funding period
Name | Used in | PP | Description | Model |
Air Conditioner System | Rl | yes | ||
Aircraft Collision Avoidance Protocol | H1/2 | no | ||
Arbiter | R3 | no | n.a. | |
Automated Rail Cars System | S2 | yes | ||
Automatic Task Allocation in Distributed Systems | R2 | yes | n.a. | |
Car Platooning | S2 | yes | ||
Car Window Lifting | H3 | yes | ||
Elastic Train Control | H1/2 | no | n.a. | |
Emergency Messages in ETCS | R1 | yes | ||
ETCS Application Level 2 | S3 | no | n.a. | |
ETCS Break Risk Assessment | S3 | no | n.a. | |
ETCS Level 3 | S2 | yes | n.a. | |
Fault-Tolerant Workstation Cluster | S3 | no | n.a. | |
FFB | S1 | yes | ||
Fischer Protocol | R3 | yes | ||
Flap controller | H3 | no | n.a. | |
Flexray | S1 | no | soon | |
Flight Control System | H3 | yes | ||
Formats | S1 | no | soon | |
Garay/MacKenzie Protocol | S1 | yes | ||
GPS Controller | S1, R3 | no | soon | |
GPS Controller 2 | S1, R3 | no | soon | |
Hanoi | R3 | no | n.a. | |
Kanban Production System | S3 | no | n.a. | |
Mutual Exclusion | R3 | yes | ||
Mutual Exclusion with Random Times | S3 | no | n.a. | |
Pipelined ALU | S1 | yes | ||
Production Cell | S1 | no | soon | |
Region Stable Hybrid Systems | H4 | no | n.a. | |
RTSS'10 | R2 | no | n.a. | |
Single-tracked Line Segment | R3 | yes | ||
SLAB Benchmarks | R1 | no | n.a. | |
Sliding Window | S1 | yes | ||
Stable Drive Train | H4 | yes | n.a. | |
Stable Ordinary Differential Equations | H4 | no | n.a. | |
Trainsystem | Project Area H, especially H3 | yes | ||
VIS Benchmarks | S1 | no | n.a. | |
VLIW ALU | S1 | yes | ||
External | Link to | |||
HSolver Benchmarks | ||||