Software and Computational Systems Lab

Funding by DFG-BRIDGE

1. Zhengyang Lu, Po-Chun Chien, Nian-Ze Lee, and Vijay Ganesh. Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract). In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2025. Keyword(s): Btor2 Funding: DFG-BRIDGE PDF
   Abstract

   We build the first machine-learning-based algorithm selection tool for hardware verification described in the Btor2 format. In addition to hardware verifiers, our tool also selects from a set of software verifiers to solve a given Btor2 instance, enabled by a Btor2-to-C translator. We propose two embeddings for a Btor2 instance, Bag of Keywords and Bit-Width Aggregation. Pairwise classifiers are applied for algorithm selection. Upon evaluation, our tool Btor2-Select solves 30.0% more instances and reduces PAR-2 by 50.2%, compared to the PDR implementation in the HWMCC'20 winner model checker AVR. Measured by the Shapley values, the software verifiers collectively contributed 27.2% to Btor2-Select's performance.
   BibTeX Entry

   @inproceedings{AAAI25, author = {Zhengyang Lu and Po-Chun Chien and Nian-Ze Lee and Vijay Ganesh}, title = {Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence~(AAAI)}, pages = {}, year = {2025}, pdf = {https://www.sosy-lab.org/research/pub/2025-AAAI.Algorithm_Selection_for_Word-Level_Hardware_Model_Checking_Student_Abstract.pdf}, abstract = {We build the first machine-learning-based algorithm selection tool for hardware verification described in the Btor2 format. In addition to hardware verifiers, our tool also selects from a set of software verifiers to solve a given Btor2 instance, enabled by a Btor2-to-C translator. We propose two embeddings for a Btor2 instance, Bag of Keywords and Bit-Width Aggregation. Pairwise classifiers are applied for algorithm selection. Upon evaluation, our tool Btor2-Select solves 30.0% more instances and reduces PAR-2 by 50.2%, compared to the PDR implementation in the HWMCC'20 winner model checker AVR. Measured by the Shapley values, the software verifiers collectively contributed 27.2% to Btor2-Select's performance.}, keyword = {Btor2}, doinone = {Unpublished: Last checked: 2024-11-18}, funding = {DFG-BRIDGE}, }

2. Salih Ates, Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. MoXIchecker: An Extensible Model Checker for MoXI. Technical report 2407.15551, arXiv/CoRR, March 2024. doi:10.48550/arXiv.2407.15551 Keyword(s): Btor2 Funding: DFG-CONVEY, DFG-BRIDGE Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.12787654
   Abstract

   MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB 2 language with constructs to define state-transition systems. The tool suite of MoXI provides a translator from MoXI to Btor2, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for Btor2 to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in Btor2. We present MoXIchecker, the first model checker that solves MoXI verification tasks directly. Instead of translating MoXI to lower-level languages, MoXIchecker uses the solver-agnostic library PySMT for SMT solvers as backend for its verification algorithms. MoXIchecker is extensible because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the MoXI tool suite.
   BibTeX Entry

   @techreport{TechReport24b, author = {Salih Ates and Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {{MoXIchecker}: {An} Extensible Model Checker for {MoXI}}, number = {2407.15551}, year = {2024}, doi = {10.48550/arXiv.2407.15551}, url = {https://gitlab.com/sosy-lab/software/moxichecker}, pdf = {https://arxiv.org/abs/2407.15551}, abstract = {MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB 2 language with constructs to define state-transition systems. The tool suite of MoXI provides a translator from MoXI to Btor2, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for Btor2 to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in Btor2. We present MoXIchecker, the first model checker that solves MoXI verification tasks directly. Instead of translating MoXI to lower-level languages, MoXIchecker uses the solver-agnostic library PySMT for SMT solvers as backend for its verification algorithms. MoXIchecker is extensible because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the MoXI tool suite.}, keyword = {Btor2}, artifact = {10.5281/zenodo.12787654}, funding = {DFG-CONVEY,DFG-BRIDGE}, institution = {arXiv/CoRR}, month = {March}, }