This repository contains a benchmark set for safety checking of relational action bases (RABs for short). Each file in the set consists of a RAB model specification and a corresponding (un)safety property to verify. The provided files can be immediately tested using the latest version of the MCMT model checker. We also attach a file with average execution times per benchmark specification.
MCMT is an SMT-based model checker that supports verification of infinite-state transition systems. One can download it here.
Consult MCMT's user manual for more information on the tool itself.
MCMT has to be linked to the SMT solver Yices 1 which has to be downloaded separately.
To run a file with a RAB model and test its safety, use the command line and type this: ./bin/mcmt [options] <filename>.
[1] S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. Safety Verification and Universal Invariants for Relational Action Bases. Proceedings of IJCAI 2023. To appear.