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. The starMC.ova contains the tools presented in the paper, for user evaluation and reproducibility.

PeerJ article URL: https://peerj.com/articles/cs-823/