Btor2-SelectMC is a compositional model checker for Btor2 circuits. It contains the following two components: Btor2-Select (described in selector/README.md): a machine-learning-based algorithm selector for bit-level, word-level, and software verifiers. CoVeriTeam (described in coveriteam/README.md): a library for on-demand composition and execution of verification tools. Given a Btor2 circuit, Btor2-Select picks the most suitable algorithm of a backend verifier to verify the circuit, and CoVeriTeam invokes the selected verifier (running the picked algorithm) in a containerized environment. Installation and Requirements Btor2-SelectMC relies on CoVeriTeam to coordinate the underlying analyzers. Therefore, the following dependencies are required: Linux Ubuntu 20.04 or newer Python 3.10 or newer Linux control groups (cgroups) Please also refer to selector/requirement.txt and coveriteam/README.md for the complete lists of requirements. To run the the backend verifiers, the system also has to satisfy their requirements. Usage To verify a Btor2 circuit with Btor2-SelectMC, please run: ./btor2-selectmc.py After executing the command, the verification result will be printed to the console. [INFO] Verification result: UNSAT # or SAT/UNKNOWN/ERROR UNSAT means that the safety property holds, i.e., bad in the Btor2 circuit is unreachable, whereas SAT means that the safety property can be violated. For more information, please run ./btor2-selectmc.py -h. HWMCC Submission For HWMCC 2024, Btor2-SelectMC employs the following backend verifiers (listed in verifiers/): Bit-level model checker for AIGER circuits (verification tasks translated by Btor2AIGER): ABC Word-level model checker for Btor2 circuits: AVR BtorMC Pono Software verifiers for C programs (verification tasks translated by Btor2C): CBMC CPAchecker ESBMC KLEE Additional software dependencies are required, including: GCC Java 17 To run Btor2-SelectMC's configuration for HWMCC 2024, please use the option --no-cache-update (because the backend verifiers have been bundled, and the cache does not need to be updated): ./btor2-selectmc.py --no-cache-update Notes on Measuring Resource Consumption Using BenchExec CoVeriTeam, a component of Btor2-SeletMC, uses runexec from BenchExec to limit and measure the resources of the containerized executions of the backend software analyzers. Therefore, benchmarking Btor-SelectMC using the BenchExec framework results in nested containers and requires a special setup. For systems with cgroups v1, please pass --full-access-dir /sys/fs/cgroup to runexec: runexec [runexec-flags] --full-access-dir /sys/fs/cgroup -- ./btor2-selectmc [btor2-selectmc-flags] For systems with cgroups v2, please prepend ./cgroup-init.sh to ./btor2-selectmc (see also BenchExec's documentation): runexec [runexec-flags] -- ./cgroup-init.sh ./btor2-selectmc [btor2-selectmc-flags] License Btor2-SelectMC is licensed under the Apache 2.0 License. The used submodules selector/ and coveriteam/, binaries in bin/, and the backend software analyzers (stored in cvt-cache/tools/ by default) are available under their respective licenses.