Artifact and instructions to generate experimental results for TACAS 2019 paper: Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking

This artifact contains the benchmarks and scripts needed to reproduce the experiments in the paper "Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking".The artifact is provided as a .zip archive. It consists of Python scripts for computing the diameter of the encoded benchmarks, checking their safety properties, and producing a table with results, comparable to the one in Section 7 of the paper. The scripts for computing the diameter and checking the safety properties use back-end SMT solvers (Z3 and CVC4), whose binaries are contained in the .deb package provided with the artifact. Additionally, the artifact contains two directories containing Python scripts used to encode our benchmarks.More information on how to run the experiments can be found in the README file. The licensing information is available in the LICENSE file.