Software and Computational Systems Lab

Publications about SMT

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. Heinrich Dennis Simon Lindner. Extending the Framework JavaSMT with the SMT Solver Bitwuzla and Evaluation using CPAchecker. at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Keyword(s): JavaSMT, SMT, Bitwuzla, CPAchecker PDF
   BibTeX Entry

   @misc{LindnerDefense, author = {Heinrich Dennis Simon Lindner}, title = {Extending the Framework JavaSMT with the SMT Solver Bitwuzla and Evaluation using CPAchecker}, year = {2023}, pdf = {https://www.sosy-lab.org/research/bsc/2023.Lindner.Extending_the_Framework_JavaSMT_with_the_SMT_Solver_Bitwuzla_and_Evaluation_using_CPAchecker.pdf}, keyword = {JavaSMT, SMT, Bitwuzla, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, }
3. Winnie Lilith Sofia Ros. Extending the JavaSMT Framework with the Apron Library for Numerical Abstract Domain with subsequent Usability Assessment. at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Keyword(s): Apron, SMT, Abstract Interpretation, JavaSMT PDF
   BibTeX Entry

   @misc{RosBA, author = {Winnie Lilith Sofia Ros}, title = {Extending the JavaSMT Framework with the Apron Library for Numerical Abstract Domain with subsequent Usability Assessment}, year = {2023}, pdf = {https://www.sosy-lab.org/research/bsc/2023.Ros.Extending_the_JavaSMT_Framework_with_the_Apron_Library_for_Numerical_Abstract_Domain_with_subsequent_Usability_Assessment.pdf}, keyword = {Apron, SMT, Abstract Interpretation, JavaSMT}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, }
4. Daniel Raffler. Adding the SMT solver OpenSMT2 to the JavaSMT Framework and Evaluation using CPAchecker. at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Keyword(s): SMT, JavaSMT, OpenSMT2, CPAchecker PDF
   BibTeX Entry

   @misc{RafflerBA, author = {Daniel Raffler}, title = {Adding the SMT solver OpenSMT2 to the JavaSMT Framework and Evaluation using CPAchecker}, year = {2023}, pdf = {https://www.sosy-lab.org/research/bsc/2023.Raffler.Adding_the_SMT_solver_OpenSMT2_to_the_JavaSMT_Framework_and_Evaluation_using_CPAchecker.pdf}, keyword = {SMT, JavaSMT, OpenSMT2, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, }
5. Janelle King. Implementing a Solver-Independent SMT-LIB2 Parser-Interpreter and Code-Generator for JavaSMT with Subsequent Evaluation. at LMU Munich, Bachelor's Thesis, LMU Munich, Software Systems Lab, 2023. Keyword(s): JavaSMT, SMT-LIB2, SMT, CPAchecker PDF
   BibTeX Entry

   @misc{KingBA, author = {Janelle King}, title = {Implementing a Solver-Independent SMT-LIB2 Parser-Interpreter and Code-Generator for JavaSMT with Subsequent Evaluation}, year = {2023}, pdf = {https://www.sosy-lab.org/research/bsc/2023.King.Implementing_a_Solver-Independent_SMT-LIB2_Parser-Interpreter_and_Code-Generator_for_JavaSMT_with_Subsequent_Evaluation.pdf}, keyword = {JavaSMT, SMT-LIB2, SMT, CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, venue = {LMU Munich}, }