Software and Computational Systems Lab

Publications of year 2024

1. Dirk Beyer and Ana Cavalcanti, editors. Proceedings of the 27st International Conference on Fundamental Approaches to Software Engineering (FASE). LNCS 14573, 2024. Springer. doi:10.1007/978-3-031-57259-3 Publisher's Version PDF Supplement
   BibTeX Entry

   @proceedings{FASE24, title = {Proceedings of the 27st International Conference on Fundamental Approaches to Software Engineering (FASE)}, editor = {Dirk Beyer and Ana Cavalcanti}, year = {2024}, series = {LNCS~14573}, publisher = {Springer}, isbn = {978-3-031-57258-6}, doi = {10.1007/978-3-031-57259-3}, sha256 = {}, url = {https://etaps.org/2024/conferences/fase/}, pdf = {https://doi.org/10.1007/978-3-031-57259-3}, }

1. Dirk Beyer, Po-Chun Chien, Marek Jankola, and Nian-Ze Lee. A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification. Proc. ACM Softw. Eng.(FSE), 2024. Keyword(s): CPAchecker, Software Model Checking Funding: DFG-CONVEY
   BibTeX Entry

   @article{ItpTransfer-PACMSE, author = {Dirk Beyer and Po-Chun Chien and Marek Jankola and Nian-Ze Lee}, title = {A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification}, journal = {Proc. ACM Softw. Eng.}, volume = {}, number = {FSE}, pages = {}, year = {2024}, doi = {}, url = {}, pdf = {}, presentation = {}, abstract = {}, keyword = {CPAchecker,Software Model Checking}, artifact = {}, funding = {DFG-CONVEY}, }
2. Dirk Beyer, Matthias Kettl, and Thomas Lemberger. Decomposing Software Verification Using Distributed Summary Synthesis. Proceedings of the ACM on Software Engineering, 2024. Keyword(s): CPAchecker, Software Model Checking
   BibTeX Entry

   @article{DSS-PACMSE, author = {Dirk Beyer and Matthias Kettl and Thomas Lemberger}, title = {Decomposing Software Verification Using Distributed Summary Synthesis}, journal = {Proceedings of the ACM on Software Engineering}, volume = {}, number = {}, pages = {}, year = {2024}, doi = {}, url = {}, pdf = {}, keyword = {CPAchecker,Software Model Checking}, _sha256 = {}, }
3. Dirk Beyer, Nian-Ze Lee, and Philipp Wendler. Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification. Journal of Automated Reasoning, 2024. Keyword(s): CPAchecker, Software Model Checking 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 = {}, number = {}, pages = {}, year = {2024}, doi = {}, 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}, _sha256 = {}, }

1. Dirk Beyer, Lars Grunske, Matthias Kettl, Marian Lingsch-Rosenfeld, and Moeketsi Raselimo. P3: A Dataset of Partial Program Patches. In Proc. MSR, 2024. ACM. doi:10.1145/3643991.3644889 Keyword(s): Partial Fix, Dataset, Mining Funding: DFG-IDEFIX Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10319627
   Abstract

   Identifying and fixing bugs in programs remains a challenge and is one of the most time-consuming tasks in software development. But even after a bug is identified, and a fix has been proposed by a developer or tool, it is not uncommon that the fix is incomplete and does not cover all possible inputs that trigger the bug. This can happen quite often and leads to re-opened issues and inefficiencies. In this paper, we introduce P3, a curated dataset composed of in- complete fixes. Each entry in the set contains a series of commits fixing the same underlying issue, where multiple of the intermediate commits are incomplete fixes. These are sourced from real-world open-source C projects. The selection process involves both auto- mated and manual stages. Initially, we employ heuristics to identify potential partial fixes from repositories, subsequently we validate them through meticulous manual inspection. This process ensures the accuracy and reliability of our curated dataset. We envision that the dataset will support researchers while investigating par- tial fixes in more detail, allowing them to develop new techniques to detect and fix them.
   BibTeX Entry

   @inproceedings{MSR24, author = {Dirk Beyer and Lars Grunske and Matthias Kettl and Marian Lingsch-Rosenfeld and Moeketsi Raselimo}, title = {P3: A Dataset of Partial Program Patches}, booktitle = {Proc.\ MSR}, pages = {}, year = {2024}, publisher = {ACM}, doi = {10.1145/3643991.3644889}, url = {https://gitlab.com/sosy-lab/research/data/partial-fix-dataset}, pdf = {}, abstract = {Identifying and fixing bugs in programs remains a challenge and is one of the most time-consuming tasks in software development. But even after a bug is identified, and a fix has been proposed by a developer or tool, it is not uncommon that the fix is incomplete and does not cover all possible inputs that trigger the bug. This can happen quite often and leads to re-opened issues and inefficiencies. In this paper, we introduce P3, a curated dataset composed of in- complete fixes. Each entry in the set contains a series of commits fixing the same underlying issue, where multiple of the intermediate commits are incomplete fixes. These are sourced from real-world open-source C projects. The selection process involves both auto- mated and manual stages. Initially, we employ heuristics to identify potential partial fixes from repositories, subsequently we validate them through meticulous manual inspection. This process ensures the accuracy and reliability of our curated dataset. We envision that the dataset will support researchers while investigating par- tial fixes in more detail, allowing them to develop new techniques to detect and fix them.}, keyword = {Partial Fix, Dataset, Mining}, annote = {}, artifact = {10.5281/zenodo.10319627}, funding = {DFG-IDEFIX}, }
2. Paulína Ayaziová, Dirk Beyer, Marian Lingsch-Rosenfeld, Martin Spiessl, and Jan Strejček. Software Verification Witnesses 2.0. In Proc. SPIN, LNCS , 2024. Springer. Keyword(s): Software Model Checking, Cooperative Verification, Witness-Based Validation, CPAchecker Funding: DFG-CONVEY, DFG-IDEFIX PDF Presentation Supplement
   BibTeX Entry

   @inproceedings{SPIN24c, author = {Paulína Ayaziová and Dirk Beyer and Marian Lingsch-Rosenfeld and Martin Spiessl and Jan Strejček}, title = {Software Verification Witnesses 2.0}, booktitle = {Proc.\ SPIN}, pages = {}, year = {2024}, series = {LNCS~}, publisher = {Springer}, url = {https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/}, pdf = {https://www.sosy-lab.org/research/pub/2024-SPIN.Software_Verification_Witnesses_2.0.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-11_SPIN24_Software-Verification-Witnesses-2.0.pdf}, abstract = {}, keyword = {Software Model Checking, Cooperative Verification, Witness-Based Validation, CPAchecker}, annote = {}, artifact = {}, doinone = {Unpublished: Last checked: 2024-03-25}, funding = {DFG-CONVEY,DFG-IDEFIX}, }
3. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Augmenting Interpolation-Based Model Checking with Auxiliary Invariants. In Proc. SPIN, 2024. Springer. Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY PDF Presentation Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10548594
   Abstract

   Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.
   BibTeX Entry

   @inproceedings{SPIN24b, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Augmenting Interpolation-Based Model Checking with Auxiliary Invariants}, booktitle = {Proc.\ SPIN}, pages = {}, year = {2024}, series = {}, publisher = {Springer}, url = {https://www.sosy-lab.org/research/imc-df/}, pdf = {https://www.sosy-lab.org/research/pub/2024-SPIN.Augmenting_Interpolation-Based_Model_Checking_with_Auxiliary_Invariants.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-10_SPIN_Augmenting_IMC_with_Auxiliary_Invariants_Po-Chun.pdf}, abstract = {Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including <i>k</i>-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.}, keyword = {Software Model Checking, Cooperative Verification, CPAchecker}, annote = {This article received the "Best Paper Award" at SPIN 2024! An <a href="https://www.sosy-lab.org/research/bib/All/index.html#TechReport24a">extended version</a> of this article is available on <a href="https://doi.org/10.48550/arXiv.2403.07821">arXiv</a>.}, artifact = {10.5281/zenodo.10548594}, doinone = {Unpublished: Last checked: 2024-03-16}, funding = {DFG-CONVEY}, }
   Additional Infos

   This article received the "Best Paper Award" at SPIN 2024! An extended version of this article is available on arXiv.
4. Dirk Beyer, Matthias Kettl, and Thomas Lemberger. Fault Localization on Verification Witnesses. In Proceedings of the 30th International Symposium on Model Checking Software (SPIN 2024, Luxembourg City, Luxembourg, April 10-11), LNCS, 2024. Springer. Keyword(s): Software Model Checking, Witness-Based Validation, CPAchecker Funding: DFG-CONVEY, DFG-IDEFIX, DFG-COOP PDF
   Artifact(s)

   1. doi:10.5281/zenodo.10794627
   Abstract

   When verifiers report an alarm, they export a violation witness (exchangeable counterexample) that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported alarm in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.
   BibTeX Entry

   @inproceedings{SPIN24a, author = {Dirk Beyer and Matthias Kettl and Thomas Lemberger}, title = {Fault Localization on Verification Witnesses}, booktitle = {Proceedings of the 30th International Symposium on Model Checking Software (SPIN~2024, Luxembourg City, Luxembourg, April 10-11)}, pages = {}, year = {2024}, series = {LNCS}, publisher = {Springer}, pdf = {https://sosy-lab.org/research/pub/2024-SPIN.Fault_Localization_on_Verification_Witnesses.pdf}, abstract = {When verifiers report an alarm, they export a violation witness (exchangeable counterexample) that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported alarm in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.}, keyword = {Software Model Checking, Witness-Based Validation, CPAchecker}, annote = {Nominated for best paper.<br> This work was also presented with a poster at the 46th International Conference on Software Engineering (ICSE 2024, Lisbon, Portugal, April 14-20): <a href="https://sosy-lab.org/research/pst/2024-03-05_ICSE24_Fault_Localization_on_Verification_Witnesses_Poster.pdf">Extended Abstract</a>.}, artifact = {10.5281/zenodo.10794627}, doinone = {TBD}, funding = {DFG-CONVEY,DFG-IDEFIX,DFG-COOP}, }
   Additional Infos

   Nominated for best paper.
   This work was also presented with a poster at the 46th International Conference on Software Engineering (ICSE 2024, Lisbon, Portugal, April 14-20): Extended Abstract.
5. Daniel Baier, Dirk Beyer, Po-Chun Chien, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch-Rosenfeld, Martin Spiessl, Henrik Wachowitz, and Philipp Wendler. CPAchecker 2.3 with Strategy Selection (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 359-364, 2024. Springer. doi:10.1007/978-3-031-57256-2_21 Keyword(s): Software Model Checking, Witness-Based Validation, CPAchecker Funding: DFG-CONVEY, DFG-IDEFIX Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10203297
   Abstract

   CPAchecker is a versatile framework for software verification, rooted in the established concept of configurable program analysis. Compared to the last published system description at SV-COMP 2015, the CPAchecker submission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses in CPAchecker and cover the full spectrum of the diverse program characteristics and specifications in the competition, we use strategy selection to predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses using k-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms in CPAchecker enables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories. CPAchecker also generates verification witnesses in the new YAML format.
   BibTeX Entry

   @inproceedings{TACAS24c, author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Martin Spiessl and Henrik Wachowitz and Philipp Wendler}, title = {{CPAchecker} 2.3 with Strategy Selection (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {359-364}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_21}, url = {https://cpachecker.sosy-lab.org/}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.CPAchecker_2.3_with_Strategy_Selection_Competition_Contribution.pdf}, abstract = {CPAchecker is a versatile framework for software verification, rooted in the established concept of configurable program analysis. Compared to the last published system description at SV-COMP 2015, the CPAchecker submission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses in CPAchecker and cover the full spectrum of the diverse program characteristics and specifications in the competition, we use strategy selection to predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses using <i>k</i>-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms in CPAchecker enables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories. CPAchecker also generates verification witnesses in the new YAML format.}, keyword = {Software Model Checking, Witness-Based Validation, CPAchecker}, artifact = {10.5281/zenodo.10203297}, funding = {DFG-CONVEY, DFG-IDEFIX}, }
6. Dirk Beyer. State of the Art in Software Verification and Witness Validation: SV-COMP 2024. In B. Finkbeiner and L. Kovács, editors, Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024, Luxembourg, Luxembourg, April 6-11), part 3, LNCS 14572, pages 299-329, 2024. Springer. doi:10.1007/978-3-031-57256-2_15 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{TACAS24b, author = {Dirk Beyer}, title = {State of the Art in Software Verification and Witness Validation: {SV-COMP 2024}}, booktitle = {Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2024, Luxembourg, Luxembourg, April 6-11), part~3}, editor = {B.~Finkbeiner and L.~Kovács}, pages = {299-329}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_15}, sha256 = {}, url = {https://sv-comp.sosy-lab.org/2024/}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.State_of_the_Art_in_Software_Verification_and_Witness_Validation_SV-COMP_2024.pdf}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, funding = {DFG-CONVEY}, }
7. Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee, and Nils Sirrenberg. Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers. In Proc. TACAS (3), LNCS 14572, pages 129-149, 2024. Springer. doi:10.1007/978-3-031-57256-2_7 Keyword(s): Software Model Checking, Witness-Based Validation, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10548597
   Abstract

   Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2-Cert to verify safety properties of Btor2 circuits, combining Btor2-to-C translation, software verifiers, and a new witness validator Btor2-Val, to answer the above open questions. Btor2-Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses, we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2-Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification. In our evaluation, Btor2-Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier CBMC on translated programs, it uniquely solved, with confirmed witnesses, 8% of the unsafe tasks for which the hardware verifier ABC failed to detect bugs.
   BibTeX Entry

   @inproceedings{TACAS24a, author = {Zsófia Ádám and Dirk Beyer and Po-Chun Chien and Nian-Ze Lee and Nils Sirrenberg}, title = {{Btor2-Cert}: {A} Certifying Hardware-Verification Framework Using Software Analyzers}, booktitle = {Proc.\ TACAS~(3)}, pages = {129-149}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_7}, url = {https://www.sosy-lab.org/research/btor2-cert/}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.Btor2-Cert_A_Certifying_Hardware-Verification_Framework_Using_Software_Analyzers.pdf}, abstract = {Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2-Cert to verify safety properties of Btor2 circuits, combining Btor2-to-C translation, software verifiers, and a new witness validator Btor2-Val, to answer the above open questions. Btor2-Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses, we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2-Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification. In our evaluation, Btor2-Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier CBMC on translated programs, it uniquely solved, with confirmed witnesses, 8&percnt; of the unsafe tasks for which the hardware verifier ABC failed to detect bugs.}, keyword = {Software Model Checking, Witness-Based Validation, Cooperative Verification, Btor2}, annote = {The reproduction package of this article received the "Distinguished Artifact Award" at TACAS 2024!}, artifact = {10.5281/zenodo.10548597}, funding = {DFG-CONVEY}, }
   Additional Infos

   The reproduction package of this article received the "Distinguished Artifact Award" at TACAS 2024!
8. Po-Chun Chien and Nian-Ze Lee. CPV: A Circuit-Based Program Verifier (Competition Contribution). In Proc. TACAS, LNCS 14572, pages 365-370, 2024. Springer. doi:10.1007/978-3-031-57256-2_22 Keyword(s): Software Model Checking, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10203472
   Abstract

   We submit to SV-COMP 2024 CPV, a circuit-based software verifier for C programs. CPV utilizes sequential circuits as its intermediate representation and invokes hardware model checkers to analyze the reachability safety of C programs. As the frontend, it uses Kratos2, a recently proposed verification tool, to translate a C program to a sequential circuit. As the backend, state-of-the-art hardware model checkers ABC and AVR are employed to verify the translated circuits. We configure the hardware model checkers to run various analyses, including IC3/PDR, interpolation-based model checking, and k-induction. Information discovered by hardware model checkers is represented as verification witnesses. In the competition, CPV achieved comparable performance against participants whose intermediate representations are based on control-flow graphs. In the category ReachSafety, it outperformed several mature software verifiers as a first-year participant. CPV manifests the feasibility of sequential circuits as an alternative intermediate representation for program analysis and enables head-to-head algorithmic comparison between hardware and software verification.
   BibTeX Entry

   @inproceedings{CPV-TACAS24, author = {Po-Chun Chien and Nian-Ze Lee}, title = {CPV: A Circuit-Based Program Verifier (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {365-370}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_22}, url = {https://gitlab.com/sosy-lab/software/cpv}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.CPV_A_Circuit-Based_Program_Verifier_Competition_Contribution.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-08_SVCOMP_CPV_A_Circuit-Based_Program_Verifier_Po-Chun.pdf}, abstract = {We submit to SV-COMP 2024 CPV, a circuit-based software verifier for C programs. CPV utilizes sequential circuits as its intermediate representation and invokes hardware model checkers to analyze the reachability safety of C programs. As the frontend, it uses Kratos2, a recently proposed verification tool, to translate a C program to a sequential circuit. As the backend, state-of-the-art hardware model checkers ABC and AVR are employed to verify the translated circuits. We configure the hardware model checkers to run various analyses, including IC3/PDR, interpolation-based model checking, and <i>k</i>-induction. Information discovered by hardware model checkers is represented as verification witnesses. In the competition, CPV achieved comparable performance against participants whose intermediate representations are based on control-flow graphs. In the category <i>ReachSafety</i>, it outperformed several mature software verifiers as a first-year participant. CPV manifests the feasibility of sequential circuits as an alternative intermediate representation for program analysis and enables head-to-head algorithmic comparison between hardware and software verification.}, keyword = {Software Model Checking, Cooperative Verification, Btor2}, artifact = {10.5281/zenodo.10203472}, funding = {DFG-CONVEY}, }
9. Marek Jankola and Jan Strejček. Tighter Construction of Tight Büchi Automata. 2024. Springer. Keyword(s): Büchi Automata PDF
   Abstract

   Tight automata are useful in providing the shortest coun- terexample in LTL model checking and also in constructing a maximally satisfying strategy in LTL strategy synthesis. There exists a translation of LTL formulas to tight Büchi automata and several translations of Büchi automata to equivalent tight Büchi automata. This paper presents an- other translation of Büchi automata to equivalent tight Büchi automata. The translation is designed to produce smaller tight automata and it asymptotically improves the best-known upper bound on the size of a tight Büchi automaton equivalent to a given Büchi automaton. We also provide a lower bound, which is more precise than the previously known one. Further, we show that automata reduction methods based on quo- tienting preserve tightness. Our translation was implemented in a tool called Tightener. Experimental evaluation shows that Tightener usually produces smaller tight automata than the translation from LTL to tight automata known as CGH.
   BibTeX Entry

   @inproceedings{JankolaFOSSACS2024, author = {Marek Jankola and Jan Strejček}, title = {Tighter Construction of Tight Büchi Automata}, year = {2024}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2024-FOSSACS.Tighter_Construction_of_Tight_Buchi_Automata.pdf}, abstract = {Tight automata are useful in providing the shortest coun- terexample in LTL model checking and also in constructing a maximally satisfying strategy in LTL strategy synthesis. There exists a translation of LTL formulas to tight Büchi automata and several translations of Büchi automata to equivalent tight Büchi automata. This paper presents an- other translation of Büchi automata to equivalent tight Büchi automata. The translation is designed to produce smaller tight automata and it asymptotically improves the best-known upper bound on the size of a tight Büchi automaton equivalent to a given Büchi automaton. We also provide a lower bound, which is more precise than the previously known one. Further, we show that automata reduction methods based on quo- tienting preserve tightness. Our translation was implemented in a tool called Tightener. Experimental evaluation shows that Tightener usually produces smaller tight automata than the translation from LTL to tight automata known as CGH.}, keyword = {Büchi Automata}, }

1. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version). Technical report 2403.07821, arXiv/CoRR, March 2024. doi:10.48550/arXiv.2403.07821 Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10548594
   Abstract

   Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.
   BibTeX Entry

   @techreport{TechReport24a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)}, number = {2403.07821}, year = {2024}, doi = {10.48550/arXiv.2403.07821}, url = {https://www.sosy-lab.org/research/imc-df/}, pdf = {https://arxiv.org/abs/2403.07821}, abstract = {Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including <i>k</i>-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.}, keyword = {Software Model Checking, Cooperative Verification, CPAchecker}, annote = {This technical report is an extended version of our <a href="https://www.sosy-lab.org/research/bib/All/index.html#SPIN24b">paper</a> at SPIN 2024.}, artifact = {10.5281/zenodo.10548594}, funding = {DFG-CONVEY}, institution = {arXiv/CoRR}, month = {March}, }
   Additional Infos

   This technical report is an extended version of our paper at SPIN 2024.

1. Daniel Bilic. Verification of Java Micro Services based on OpenAPI Specifications. Master's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking
   BibTeX Entry

   @misc{BilicOpenAPI, author = {Daniel Bilic}, title = {Verification of Java Micro Services based on OpenAPI Specifications}, year = {2024}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
2. Robin Mattis. Verification of Micro Services based on Pact API Contracts. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{MattisMicroserviceVerification, author = {Robin Mattis}, title = {Verification of Micro Services based on Pact API Contracts}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Mattis.Verification_of_Micro_Services_based_on_Pact_API_Contracts.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
3. Nils Sirrenberg. Certifying Software Violation Witnesses for Hardware Verification Tasks via Simulation-Based Validation. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Btor2, Witness-Based Validation PDF
   BibTeX Entry

   @misc{SirrenbergBtor2ViolationWitness, author = {Nils Sirrenberg}, title = {Certifying Software Violation Witnesses for Hardware Verification Tasks via Simulation-Based Validation}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Sirrenberg.Certifying_Software_Violation_Witnesses_for_Hardware_Verification_Tasks_via_Simulation-Based_Validation.restricted.pdf}, keyword = {Btor2, Witness-Based Validation}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
4. Jiacheng Chen. Automated Verification of the C Implementation of memcached with AFL++. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{ChenMemcachedVerificationAFL, author = {Jiacheng Chen}, title = {Automated Verification of the C Implementation of memcached with AFL++}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Chen.Automated_Verification_of_the_C_Implementation_of_memcached_with_AFL++.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
5. Jinke Li. Automated Verification of the C Implementation of memcached with Goblint. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{LiMemcachedVerificationGoblint, author = {Jinke Li}, title = {Automated Verification of the C Implementation of memcached with Goblint}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Li.Automated_Verification_of_the_C_Implementation_of_memcached_with_Goblint.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
6. Khac Ming Le. Automated Verification of the C Implementation of memcached with FuSeBMC. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{LeMemcachedVerificationFuSeBMC, author = {Khac Ming Le}, title = {Automated Verification of the C Implementation of memcached with FuSeBMC}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Le.Automated_Verification_of_the_C_Implementation_of_memcached_with_FuSeBMC.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
7. Enno Muehlbauer. Automated Verification of the C Implementation of memcached with Ultimate Automizer. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{MuehlbauerMemcachedVerificationUAutomizer, author = {Enno Muehlbauer}, title = {Automated Verification of the C Implementation of memcached with Ultimate Automizer}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Muehlbauer.Automated_Verification_of_the_C_Implementation_of_memcached_with_Ultimate_Automizer.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
8. Karim Triki. Automated Verification of the C Implementation of memcached with Taipan. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{TrikiMemcachedVerificationTaipan, author = {Karim Triki}, title = {Automated Verification of the C Implementation of memcached with Taipan}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Triki.Automated_Verification_of_the_C_Implementation_of_memcached_with_Taipan.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
9. Ahmad Ghanem. Automated Verification of the C Implementation of memcached with ESBMC. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
   BibTeX Entry

   @misc{GhanemMemcachedVerificationESBMC, author = {Ahmad Ghanem}, title = {Automated Verification of the C Implementation of memcached with ESBMC}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Ghanem.Automated_Verification_of_the_C_Implementation_of_memcached_with_ESBMC.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
10. Yu-Chieh Lin. Automated Verification of the C Implementation of memcached with CPAchecker and k-Induction. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{LinMemcachedVerificationCPAchecker, author = {Yu-Chieh Lin}, title = {Automated Verification of the C Implementation of memcached with CPAchecker and k-Induction}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Lin.Automated_Verification_of_the_C_Implementation_of_memcached_with_CPAchecker_and_K-Induction.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
11. Kai Müller. Automated Verification of the C Implementation of memcached with Klee. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{MuellerMemcachedVerificationKlee, author = {Kai Müller}, title = {Automated Verification of the C Implementation of memcached with Klee}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Mueller.Automated_Verification_of_the_C_Implementation_of_memcached_with_Klee.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
12. Rania Qteishat. Automated Verification of the C Implementation of memcached with CBMC. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{QteishatMemcachedVerificationCBMC, author = {Rania Qteishat}, title = {Automated Verification of the C Implementation of memcached with CBMC}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Qteishat.Automated_Verification_of_the_C_Implementation_of_memcached_with_CBMC.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
13. Dinghao Shi. Automated Verification of the C Implementation of memcached with AFL++. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{ShiMemcachedVerificationAFL, author = {Dinghao Shi}, title = {Automated Verification of the C Implementation of memcached with AFL++}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Shi.Automated_Verification_of_the_C_Implementation_of_memcached_with_AFL++.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
14. Tong Wu. Automated Verification of the C Implementation of memcached with Goblint. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{WuMemcachedVerificationGoblint, author = {Tong Wu}, title = {Automated Verification of the C Implementation of memcached with Goblint}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Wu.Automated_Verification_of_the_C_Implementation_of_memcached_with_Goblint.restricted.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
15. Marko Ristic. A Library for Unit Verification. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2024. Keyword(s): Software Model Checking PDF
    BibTeX Entry

    @misc{RisticUnitVerification, author = {Marko Ristic}, title = {A Library for Unit Verification}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Ristic.A_Library_for_Unit_Verification.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }