Bibliographic record
Abstract
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.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.003 | 0.010 |
| Meta-epidemiology (narrow) | 0.002 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.001 | 0.001 |
| Scholarly communication | 0.002 | 0.003 |
| Open science | 0.003 | 0.003 |
| Research integrity | 0.002 | 0.002 |
| Insufficient payload (model declined to judge) | 0.327 | 0.172 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; the direct Gemma label and the distilled Codex classifier agree on what is shown here.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".