We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
2 papers accepted at ASE 2024: BenchCloud and CoVeriTeam GUI

Funding by DFG-BRIDGE

Articles in conference or workshop proceedings

  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. Link to this entry 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. In Proc. VSTTE, 2024. Springer. Link to this entry Keyword(s): Btor2 Funding: DFG-CONVEY, DFG-BRIDGE PDF Supplement
    Artifact(s)
    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}, pages = {}, year = {2024}, series = {}, publisher = {Springer}, doi = {}, 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 = {Btor2}, artifact = {10.5281/zenodo.13895872}, funding = {DFG-CONVEY, DFG-BRIDGE}, }

Internal reports

  1. 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 Link to this entry Keyword(s): Btor2 Funding: DFG-CONVEY, DFG-BRIDGE Publisher's Version PDF Supplement
    Artifact(s)
    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}, }

Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Last modified: Wed Dec 04 15:42:47 2024 UTC