Replication Package (Virtual Machine) for article "starMC: an automata based CTL* model checker"

This package is a virtual machine (VM) to execute the starMC programs and benchmark. The system setup is described in the research article "starMC: an automata based CTL* model checker", being published at PeerJ Computer Science (currently accepted). The virtual machine contains both tools and data to reproduce a CTL* model checking logic benchmark. CTL* is a formal logic for the verification of temporal properties of programs. The benchmark is a collection of 1018 model instances (encoded as Petri nets), derived from the Model Checking Context benchmark (https://mcc.lip6.fr/), and about 60.000 CTL, LTL and CTL* queries. It is currently the only large-scale CTL* benchmark for Petri nets publicly available. The starMC-benchmark.ova VM is configured to use 4 CPU cores and 16 GB of RAM. The VM was created with VirtualBox version 5, and tested on a host machine with an 8-core Xeon CPU and 32 GB of RAM. The VM uses the Ubuntu 20 OS, and username and password are both "user". The home directory contains a README file with instructions on how to run the tools, where the benchmark data (models, queries, variable orders) are found, and the script to reproduce the plots in the paper.<br> The starMC.ova contains the tools presented in the paper, for user evaluation and reproducibility.