Btor2-SelectMC (HWMCC 2024 Submission)
Notice bibliographique
Résumé
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.
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Comment cette classification a été obtenuedéplier
Prédiction machine sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Le volet Gemma est une étiquette directe du modèle pour chaque travail de la base, lue sur la notice réduite au titre. Le volet Codex est un classifieur appris des 10 348 étiquettes directes de Codex et calibré sur les taux pondérés de l'échantillon; les champs sans appui suffisant ne portent aucun appel Codex. Le mode candidate est l'union des deux volets; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont pas des étiquettes humaines.
Scores du classifieur distillé par catégorie (deux têtes)
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,003 | 0,010 |
| Méta-épidémiologie (sens strict) | 0,002 | 0,001 |
| Méta-épidémiologie (sens large) | 0,001 | 0,001 |
| Bibliométrie | 0,001 | 0,001 |
| Études des sciences et des technologies | 0,001 | 0,001 |
| Communication savante | 0,002 | 0,003 |
| Science ouverte | 0,003 | 0,003 |
| Intégrité de la recherche | 0,002 | 0,002 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,327 | 0,172 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découleClassification
machine, non validéePrédiction automatique; l’étiquette directe de Gemma et le classifieur distillé Codex s’accordent sur ce qui est montré ici.
Le détail, modèle par modèle et score par score, se trouve en fin de page sous « Comment cette classification a été obtenue ».