Software and Computational Systems Lab

Funding by DFG-BRIDGE

1. Salih Ates, Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. MoXIchecker: An Extensible Model Checker for MoXI. In Proc. VSTTE 2024, LNCS 15525, pages 1-14, 2025. Springer. doi:10.1007/978-3-031-86695-1_1 Keyword(s): SMT, Btor2, MoXIchecker Funding: DFG-CONVEY, DFG-BRIDGE Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.13895872
   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

   @inproceedings{VSTTE24, author = {Salih Ates and Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {{MoXIchecker}: {An} Extensible Model Checker for {MoXI}}, booktitle = {Proc.\ VSTTE 2024}, pages = {1-14}, year = {2025}, series = {LNCS~15525}, publisher = {Springer}, doi = {10.1007/978-3-031-86695-1_1}, url = {https://www.sosy-lab.org/research/moxichecker/}, pdf = {https://www.sosy-lab.org/research/pub/2024-VSTTE.MoXIchecker_An_Extensible_Model_Checker_for_MoXI.pdf}, presentation = {}, 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 = {SMT, Btor2, MoXIchecker}, artifact = {10.5281/zenodo.13895872}, funding = {DFG-CONVEY, DFG-BRIDGE}, }
2. Zhengyang Lu, Po-Chun Chien, Nian-Ze Lee, Arie Gurfinkel, and Vijay Ganesh. Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking. In Proceedings of the International Conference on Computer Aided Verification (CAV), LNCS, 2025. Springer. Keyword(s): Btor2 Funding: DFG-BRIDGE PDF Supplement
   Abstract

   In recent years, a diverse variety of hardware model-checking tools and techniques that exhibit complementary strengths and distinct weaknesses have been proposed. This state of affairs naturally suggests the use of algorithm selection techniques to select the right tool for a given instance. To automate this process, we present Btor2-Select, a machine learning-based algorithm-selection framework for the hardware model-checking problem described in the word-level modeling language Btor2. The framework offers an efficient and effective machine-learning pipeline for training an algorithm selector. Btor2-Select also enables the use of the trained selector to predict the most suitable off-the-shelf model checker for a given verification task and automatically invoke it to solve the task. Evaluated on a comprehensive Btor2 benchmark suite coupled with a set of state-of-the-art model checkers, Btor2-Select trained an algorithm selector that successfully closed over 65 % of the PAR-2 performance gap between the best single tool and the idealized virtual selector. Moreover, the selector outperformed a portfolio model checker that runs three complementary leading verification engines in parallel. Btor2-Select offers a simple, systematic, and extensible solution to harness the complementary strengths of diverse model checkers. With its fast and highly configurable training procedure, Btor2-Select can be easily integrated with new tools and applied to various application domains.
   BibTeX Entry

   @inproceedings{Btor2Select-CAV25, author = {Zhengyang Lu and Po-Chun Chien and Nian-Ze Lee and Arie Gurfinkel and Vijay Ganesh}, title = {\textsc{Btor2-Select}: {Machine} Learning Based Algorithm Selection for Hardware Model Checking}, booktitle = {Proceedings of the International Conference on Computer Aided Verification~(CAV)}, pages = {}, year = {2025}, series = {LNCS}, publisher = {Springer}, doi = {}, url = {https://www.sosy-lab.org/research/btor2-select/}, pdf = {https://www.sosy-lab.org/research/pub/2025-CAV.Btor2-Select_Machine_Learning_Based_Algorithm_Selection_for_Hardware_Model_Checking.pdf}, abstract = {In recent years, a diverse variety of hardware model-checking tools and techniques that exhibit complementary strengths and distinct weaknesses have been proposed. This state of affairs naturally suggests the use of algorithm selection techniques to select the right tool for a given instance. To automate this process, we present Btor2-Select, a machine learning-based algorithm-selection framework for the hardware model-checking problem described in the word-level modeling language Btor2. The framework offers an efficient and effective machine-learning pipeline for training an algorithm selector. Btor2-Select also enables the use of the trained selector to predict the most suitable off-the-shelf model checker for a given verification task and automatically invoke it to solve the task. Evaluated on a comprehensive Btor2 benchmark suite coupled with a set of state-of-the-art model checkers, Btor2-Select trained an algorithm selector that successfully closed over 65 % of the PAR-2 performance gap between the best single tool and the idealized virtual selector. Moreover, the selector outperformed a portfolio model checker that runs three complementary leading verification engines in parallel. Btor2-Select offers a simple, systematic, and extensible solution to harness the complementary strengths of diverse model checkers. With its fast and highly configurable training procedure, Btor2-Select can be easily integrated with new tools and applied to various application domains.}, keyword = {Btor2}, funding = {DFG-BRIDGE}, }
3. 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), pages 29426-29427, 2025. doi:10.1609/aaai.v39i28.35275 Keyword(s): Btor2 Funding: DFG-BRIDGE Publisher's Version PDF Supplement
   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{Btor2Select-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)}, volume = {39}, number = {28}, pages = {29426-29427}, year = {2025}, doi = {10.1609/aaai.v39i28.35275}, url = {https://gitlab.com/sosy-lab/software/btor2-select}, 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}, funding = {DFG-BRIDGE}, }

4. Salih Ates, Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. MoXIchecker: An Extensible Model Checker for MoXI. Technical report 2407.15551, arXiv/CoRR, July 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 = {July}, }