Software and Computational Systems Lab

Publications of year 2025

1. Dirk Beyer, Nian-Ze Lee, and Philipp Wendler. Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification. Journal of Automated Reasoning, 69, 2025. doi:10.1007/s10817-024-09702-9 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
   BibTeX Entry

   @article{IMC-JAR, author = {Dirk Beyer and Nian-Ze Lee and Philipp Wendler}, title = {Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification}, journal = {Journal of Automated Reasoning}, volume = {69}, number = {}, pages = {}, year = {2025}, doi = {10.1007/s10817-024-09702-9}, sha256 = {6b9fbdc907a13630dc933f9e947dbd3c345acaf7b8de0595348360eb98dcbbfc}, url = {https://www.sosy-lab.org/research/cpa-imc/}, pdf = {https://www.sosy-lab.org/research/pub/2024-JAR.Interpolation_and_SAT-Based_Model_Checking_Revisited_Adoption_to_Software_Verification.pdf}, keyword = {CPAchecker,Software Model Checking}, }
2. Dirk Beyer and Thomas Lemberger. Six Years Later: Testing vs. Model Checking. International Journal on Software Tools for Technology Transfer (STTT):633-646, 2025. doi:10.1007/s10009-024-00769-8 Keyword(s): Benchmarking, Competition on Software Verification (SV-COMP), Competition on Software Testing (Test-Comp), Software Model Checking, Software Testing Funding: DFG-COOP Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.10232648
   Abstract

   Six years ago, we performed the first large-scale comparison of automated test generators and software model checkers with respect to bug-finding capabilities on a benchmark set with 5 693 C programs. Since then, the International Competition on Software Testing (Test-Comp) has established standardized formats and community-agreed rules for the experimental comparison of test generators. With this new context, it is time to revisit our initial question: Model checkers or test generators—which tools are more effective in finding bugs in software? To answer this, we perform a comparative analysis on the tools and existing data published by two competitions, the International Competition on Software Verification (SV-COMP) and Test-Comp. The results provide two insights: (1) Almost all test generators that participate in Test-Comp use hybrid approaches that include formal methods, and (2) while the considered model checkers are still highly competitive, they are now outperformed by the bug-finding capabilities of the considered test generators.
   BibTeX Entry

   @article{TestStudy-STTT, author = {Dirk Beyer and Thomas Lemberger}, title = {Six Years Later: Testing vs. Model Checking}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {}, number = {}, pages = {633-646}, year = {2025}, doi = {10.1007/s10009-024-00769-8}, sha256 = {54a77a871b92516db8785b627ee73ef48f110616b368afb9554e0b71832e47c5}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2024-STTT.Six_Years_Later_Testing_vs_Model_Checking.pdf}, presentation = {}, abstract = {Six years ago, we performed the first large-scale comparison of automated test generators and software model checkers with respect to bug-finding capabilities on a benchmark set with 5 693 C programs. Since then, the International Competition on Software Testing (Test-Comp) has established standardized formats and community-agreed rules for the experimental comparison of test generators. With this new context, it is time to revisit our initial question: Model checkers or test generators—which tools are more effective in finding bugs in software? To answer this, we perform a comparative analysis on the tools and existing data published by two competitions, the International Competition on Software Verification (SV-COMP) and Test-Comp. The results provide two insights: (1) Almost all test generators that participate in Test-Comp use hybrid approaches that include formal methods, and (2) while the considered model checkers are still highly competitive, they are now outperformed by the bug-finding capabilities of the considered test generators.}, keyword = {Benchmarking, Competition on Software Verification (SV-COMP), Competition on Software Testing (Test-Comp), Software Model Checking, Software Testing}, artifact = {10.5281/zenodo.10232648}, funding = {DFG-COOP}, }

3. Salih Ates, Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. MoXIchecker: An Extensible Model Checker for MoXI. In Proc. VSTTE, LNCS 15525, 2025. Springer. Keyword(s): Btor2 Funding: DFG-CONVEY, DFG-BRIDGE 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}, pages = {}, year = {2025}, series = {LNCS~15525}, publisher = {Springer}, 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}, doinone = {Unpublished: Last checked: 2025-02-08}, funding = {DFG-CONVEY, DFG-BRIDGE}, }
4. Thomas Lemberger and Henrik Wachowitz. Nacpa: Native Checking with Parallel-Portfolio Analyses (Competition Contribution). In Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025, Hamilton, Canada, May 3-8), 2025. Springer. Keyword(s): Software Model Checking, CPAchecker Funding: DFG-CONVEY
   Artifact(s)

   1. doi:10.5281/zenodo.14203473
   BibTeX Entry

   @inproceedings{TACAS25-Nacpa, author = {Thomas Lemberger and Henrik Wachowitz}, title = {{Nacpa}: Native Checking with Parallel-Portfolio Analyses (Competition Contribution)}, booktitle = {Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2025, Hamilton, Canada, May 3-8)}, pages = {}, year = {2025}, series = {}, publisher = {Springer}, keyword = {Software Model Checking, CPAchecker}, artifact = {10.5281/zenodo.14203473}, doinone = {Unpublished: Last checked: 2025-01-22}, funding = {DFG-CONVEY}, }
5. 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}, }

6. Noah König. Modular Partial Order Reduction in Software Verification. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2025. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{KoenigModularPOR, author = {Noah König}, title = {Modular Partial Order Reduction in Software Verification}, year = {2025}, pdf = {https://www.sosy-lab.org/research/bsc/2025.Koenig.Modular_Partial_Order_Reduction_in_Software_Verification.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
7. Maximilian Beer. Using Machine Learning To Infer Predicates For Software Verification. Master's Thesis, LMU Munich, Software Systems Lab, 2025. Keyword(s): Witnesses PDF
   BibTeX Entry

   @misc{BeerMachineLearningPredicates, author = {Maximilian Beer}, title = {Using Machine Learning To Infer Predicates For Software Verification}, year = {2025}, pdf = {https://www.sosy-lab.org/research/msc/2025.Beer.Using_Machine_Learning_To_Infer_Predicates_For_Software_Verification.restricted.pdf}, keyword = {Witnesses}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
8. Moritz Auer. Finding Semantically Equivalent Correctness Witnesses. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2025. Keyword(s): Witnesses PDF
   BibTeX Entry

   @misc{AuerSemanticallyEquivalentWitnesses, author = {Moritz Auer}, title = {Finding Semantically Equivalent Correctness Witnesses}, year = {2025}, pdf = {https://www.sosy-lab.org/research/bsc/2025.Auer.Finding_Semantically_Equivalent_Correctness_Witnesses.restricted.pdf}, keyword = {Witnesses}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
9. Marcel Bernert. Concolic Execution with Generational Search in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2025.
   BibTeX Entry

   @misc{GenrationalSearch, author = {Marcel Bernert}, title = {Concolic Execution with Generational Search in CPAchecker}, year = {2025}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }