Verified Model Checking of Timed Automata

This is the project page corresponding to our TACAS 18 paper.

Benchmarks

The Uppaal benchmarks are not contained in the artifact below but can be downloaded here.
The benchmarks were run with the following configuration options:

• For Uppaal_1: UPPAAL_OLD_SYNTAX=1 verifyta -n 2 -u -d -s benchmark.ta
• and Uppaal_2: UPPAAL_OLD_SYNTAX=1 verifyta -n 3 -u -d -s benchmark.ta

Tested against Uppaal version 4.1.19. The benchmarks are derived from these.

Artifact

Download artifact!