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

Publications about Cooperative Verification

Articles in journal or book chapters
  1. Jan Haltermann, Marie-Christine Jakobs, Cedric Richter, and Heike Wehrheim. Parallel program analysis on path ranges. Science of Computer Programming, 238, 2024. doi:10.1016/j.scico.2024.103154 Link to this entry Keyword(s): Ranged Program Analysis, Cooperative Verification, Software Model Checking, CPAchecker Funding: DFG-COOP Publisher's Version
    Artifact(s)
    BibTeX Entry
    @article{RangedPA-journal, author = {Jan Haltermann and Marie{-}Christine Jakobs and Cedric Richter and Heike Wehrheim}, title = {Parallel program analysis on path ranges}, journal = {Science of Computer Programming}, volume = {238}, year = {2024}, doi = {10.1016/j.scico.2024.103154}, url = {}, pdf = {}, keyword = {Ranged Program Analysis, Cooperative Verification, Software Model Checking, CPAchecker}, artifact = {10.5281/zenodo.8398988}, funding = {DFG-COOP}, }
  2. Thomas Lemberger. Cooperative Approaches Across Test Generation and Formal Software Verification. Softwaretechnik-Trends, 44(2):66-67, July 2024. Gesellschaft für Informatik, Berlin. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification PDF
    BibTeX Entry
    @article{SW-Trends24, author = {Thomas Lemberger}, title = {Cooperative Approaches Across Test Generation and Formal Software Verification}, journal = {Softwaretechnik-Trends}, volume = {44}, number = {2}, pages = {66-67}, year = {2024}, publisher = {Gesellschaft f{\"u}r Informatik, Berlin}, pdf = {https://www.sosy-lab.org/research/pub/2024-SWT.Cooperatives_Approaches_Across_Test_Generation_and_Formal_Software_Verification.pdf}, keyword = {Software Model Checking, Cooperative Verification}, annote = {Summary of dissertation}, doinone = {DOI not available}, issn = {0720-8928}, month = {July}, }
    Additional Infos
    Summary of dissertation

Articles in conference or workshop proceedings
  1. Dirk Beyer, Thomas Lemberger, and Henrik Wachowitz. CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers. In Proceedings of the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2024, Kyoto, Japan, October 21-24), LNCS , 2024. Springer. Link to this entry Keyword(s): CPAchecker, Software Model Checking, Cooperative Verification Funding: DFG-CONVEY PDF
    Artifact(s)
    BibTeX Entry
    @inproceedings{ATVA24, author = {Dirk Beyer and Thomas Lemberger and Henrik Wachowitz}, title = {{CPA-Daemon}: Mitigating Tool Restarts for Java-Based Verifiers}, booktitle = {Proceedings of the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA~2024, Kyoto, Japan, October 21-24)}, pages = {}, year = {2024}, series = {LNCS~}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2024-ATVA.CPA-Daemon_Mitigating_Tool_Restart_for_Java-Based_Verifiers.pdf}, abstract = {}, keyword = {CPAchecker, Software Model Checking, Cooperative Verification}, artifact = {https://doi.org/10.5281/zenodo.11147333}, doinone = {Unpublished: Last checked: 2024-10-01}, funding = {DFG-CONVEY}, }
  2. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Augmenting Interpolation-Based Model Checking with Auxiliary Invariants. In Proceedings of the 30th International Symposium on Model Checking Software (SPIN 2024, Luxembourg City, Luxembourg, April 10-11), LNCS 14624, pages 227-247, 2024. Springer. doi:10.1007/978-3-031-66149-5_13 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    Artifact(s)
    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{SPIN24c, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Augmenting Interpolation-Based Model Checking with Auxiliary Invariants}, booktitle = {Proceedings of the 30th International Symposium on Model Checking Software (SPIN~2024, Luxembourg City, Luxembourg, April 10-11)}, pages = {227-247}, year = {2024}, series = {LNCS~14624}, publisher = {Springer}, doi = {10.1007/978-3-031-66149-5_13}, 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}, 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.
  3. Paulína Ayaziová, Dirk Beyer, Marian Lingsch-Rosenfeld, Martin Spiessl, and Jan Strejček. Software Verification Witnesses 2.0. In Proceedings of the 30th International Symposium on Model Checking Software (SPIN 2024, Luxembourg City, Luxembourg, April 10-11), LNCS 14624, pages 184-203, 2024. Springer. doi:10.1007/978-3-031-66149-5_11 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Witness-Based Validation, Witness-Based Validation (main), CPAchecker Funding: DFG-CONVEY, DFG-IDEFIX Publisher's Version PDF Presentation Supplement
    Artifact(s)
    BibTeX Entry
    @inproceedings{SPIN24a, 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 = {Proceedings of the 30th International Symposium on Model Checking Software (SPIN~2024, Luxembourg City, Luxembourg, April 10-11)}, pages = {184-203}, year = {2024}, series = {LNCS~14624}, publisher = {Springer}, doi = {10.1007/978-3-031-66149-5_11}, 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, Witness-Based Validation (main), CPAchecker}, annote = {}, artifact = {10.5281/zenodo.10826204}, funding = {DFG-CONVEY,DFG-IDEFIX}, }
  4. 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 Link to this entry Keyword(s): Software Model Checking, Witness-Based Validation, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    Artifact(s)
    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/}, 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}, _pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.Btor2-Cert_A_Certifying_Hardware-Verification_Framework_Using_Software_Analyzers.pdf}, 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!
  5. Jan Haltermann, Marie-Christine Jakobs, Cedric Richter, and Heike Wehrheim. Ranged Program Analysis: A Parallel Divide-and-Conquer Approach for Software Verification. In Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, February 26 - March 1, 2024, LNI P-343, pages 157-158, 2024. GI. doi:10.18420/SW2024_52 Link to this entry Keyword(s): Ranged Program Analysis, Cooperative Verification, Software Model Checking, CPAchecker Publisher's Version
    BibTeX Entry
    @inproceedings{JakobsSE2024, author = {Jan Haltermann and Marie{-}Christine Jakobs and Cedric Richter and Heike Wehrheim}, title = {Ranged Program Analysis: A Parallel Divide-and-Conquer Approach for Software Verification}, booktitle = {Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, February 26 - March 1, 2024}, pages = {157-158}, year = {2024}, series = {{LNI}~{P-343}}, publisher = {GI}, doi = {10.18420/SW2024_52}, pdf = {}, keyword = {Ranged Program Analysis, Cooperative Verification, Software Model Checking, CPAchecker}, annote = {}, artifact = {}, funding = {}, }
  6. Thomas Lemberger and Henrik Wachowitz. CoVeriTeam GUI: A No-Code Approach to Cooperative Software Verification. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024, Sacramento, CA, USA, October 27-November 1), pages 2419-2422, 2024. doi:10.1145/3691620.3695366 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification Funding: DFG-CONVEY Publisher's Version PDF
    Artifact(s)
    Abstract
    We present CoVeriTeam GUI, a No-Code web frontend to compose new software-verification workflows from existing analysis techniques. Verification approaches stopped relying on single techniques years ago, and instead combine selections that complement each other well. So far, such combinations were-under high implementation and maintenance cost-glued together with proprietary code. Now, CoVeriTeam GUI enables users to build new verification workflows without programming. Verification techniques can be combined through various composition operators in a drag-and-drop fashion directly in the browser, and an integration with a remote service allows to execute the built workflows with the click of a button. CoVeriTeam GUI is available open source under Apache 2.0: https://gitlab.com/sosy-lab/software/coveriteam-gui
    Demonstration video: https://youtu.be/oZoOARuIOuA
    BibTeX Entry
    @inproceedings{CoVeriTeamGUI-ASE24, author = {Thomas Lemberger and Henrik Wachowitz}, title = {CoVeriTeam GUI: A No-Code Approach to Cooperative Software Verification}, booktitle = {Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024, Sacramento, CA, USA, October 27-November 1)}, pages = {2419-2422}, year = {2024}, doi = {10.1145/3691620.3695366}, pdf = {https://www.sosy-lab.org/research/pub/2024-ASE24.CoVeriTeam_GUI_A_No-Code_Approach_to_Cooperative_Software_Verification.pdf}, presentation = {}, abstract = {We present CoVeriTeam GUI, a No-Code web frontend to compose new software-verification workflows from existing analysis techniques. Verification approaches stopped relying on single techniques years ago, and instead combine selections that complement each other well. So far, such combinations were---under high implementation and maintenance cost---glued together with proprietary code. Now, CoVeriTeam GUI enables users to build new verification workflows without programming. Verification techniques can be combined through various composition operators in a drag-and-drop fashion directly in the browser, and an integration with a remote service allows to execute the built workflows with the click of a button. CoVeriTeam GUI is available open source under Apache 2.0: <a href="https://gitlab.com/sosy-lab/software/coveriteam-gui">https://gitlab.com/sosy-lab/software/coveriteam-gui</a><br> Demonstration video: <a href="https://youtu.be/oZoOARuIOuA">https://youtu.be/oZoOARuIOuA</a>}, keyword = {Software Model Checking, Cooperative Verification}, artifact = {10.5281/zenodo.13757771}, funding = {DFG-CONVEY}, }
  7. 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 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    Artifact(s)
    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}, }
  8. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification. In Proc. ASE, pages 2050-2053, 2023. IEEE. doi:10.1109/ASE56229.2023.00213 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF Presentation Video Supplement
    Artifact(s)
    Abstract
    Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the k-induction implementation in CPAchecker, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on SV-Benchmarks, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain k-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain k-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized k-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use CoVeriTeam, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20%.
    Demonstration video: https://youtu.be/l7UG-vhTL_4
    BibTeX Entry
    @inproceedings{ASE23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {{CPA-DF}: {A} Tool for Configurable Interval Analysis to Boost Program Verification}, booktitle = {Proc.\ ASE}, pages = {2050-2053}, year = {2023}, series = {}, publisher = {IEEE}, doi = {10.1109/ASE56229.2023.00213}, url = {https://www.sosy-lab.org/research/cpa-df/}, pdf = {https://www.sosy-lab.org/research/pub/2023-ASE.CPA-DF_A_Tool_for_Configurable_Interval_Analysis_to_Boost_Program_Verification.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2023-09-13_ASE_CPA-DF_Po-Chun.pdf}, abstract = {Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the <i>k</i>-induction implementation in <a href="https://cpachecker.sosy-lab.org/">CPAchecker</a>, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on <a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks">SV-Benchmarks</a>, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain <i>k</i>-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain <i>k</i>-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized <i>k</i>-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use <a href="https://gitlab.com/sosy-lab/software/coveriteam">CoVeriTeam</a>, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20&percnt;. <br> Demonstration video: <a href="https://youtu.be/l7UG-vhTL_4">https://youtu.be/l7UG-vhTL_4</a>}, keyword = {Software Model Checking, Cooperative Verification, CPAchecker}, artifact = {10.5281/zenodo.8245821}, funding = {DFG-CONVEY}, video = {https://youtu.be/l7UG-vhTL_4}, }
  9. Dirk Beyer, Sudeep Kanav, and Henrik Wachowitz. CoVeriTeam Service: Verification as a Service. In Proc. ICSE, pages 21-25, 2023. IEEE. doi:10.1109/ICSE-Companion58688.2023.00017 Link to this entry Keyword(s): Software Model Checking, Incremental Verification, Cooperative Verification Funding: DFG-CONVEY, DFG-COOP Publisher's Version PDF Supplement
    Artifact(s)
    Abstract
    The research community has developed numerous tools for solving verification problems, but we are missing a common interface for executing them. This means users have to spend considerable effort on the installation and parameter setup, for each new tool (version) they want to execute. The situation could make a verification researcher wanting to experiment with a new verification tool turn away from it. We aim to make it easier for users to execute verification tools, as well as provide mechanism for tool developers to make their tools easily accessible. Our solution combines a web service and a common interface for verification tools. The presented service has been used during the 2023 competitions on software verification and testing, for integration testing. As another use- case, we developed a service for incremental verification on top of the CoVeriTeam Service and demonstrate its use in a continuous-integration process.
    BibTeX Entry
    @inproceedings{ICSE23, author = {Dirk Beyer and Sudeep Kanav and Henrik Wachowitz}, title = {{CoVeriTeam Service}: {Verification} as a Service}, booktitle = {Proc.\ ICSE}, pages = {21-25}, year = {2023}, publisher = {IEEE}, doi = {10.1109/ICSE-Companion58688.2023.00017}, url = {https://coveriteam-service.sosy-lab.org/static/index.html}, pdf = {https://www.sosy-lab.org/research/pub/2023-ICSE.CoVeriTeam_Service_Verification_as_a_Service.pdf}, abstract = {The research community has developed numerous tools for solving verification problems, but we are missing a common interface for executing them. This means users have to spend considerable effort on the installation and parameter setup, for each new tool (version) they want to execute. The situation could make a verification researcher wanting to experiment with a new verification tool turn away from it. We aim to make it easier for users to execute verification tools, as well as provide mechanism for tool developers to make their tools easily accessible. Our solution combines a web service and a common interface for verification tools. The presented service has been used during the 2023 competitions on software verification and testing, for integration testing. As another use- case, we developed a service for incremental verification on top of the {CoVeriTeam} Service and demonstrate its use in a continuous-integration process.}, keyword = {Software Model Checking,Incremental Verification,Cooperative Verification}, _sha256 = {604dd391b6a49e46e97b6faafbb3cc331ccf5c04e3d364cf1e76a2c99c1c267f}, artifact = {10.5281/zenodo.7276532}, funding = {DFG-CONVEY,DFG-COOP}, }
  10. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator. In Proc. TACAS, LNCS 13994, pages 152-172, 2023. Springer. doi:10.1007/978-3-031-30820-8_12 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2 Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    Artifact(s)
    Abstract
    Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a converter from word-level sequential circuits to C programs. We choose the Btor2 language as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.
    BibTeX Entry
    @inproceedings{TACAS23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Bridging Hardware and Software Analysis with {Btor2C}: {A} Word-Level-Circuit-to-{C} Translator}, booktitle = {Proc.\ TACAS}, pages = {152-172}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_12}, url = {https://www.sosy-lab.org/research/btor2c/}, presentation = {https://www.sosy-lab.org/research/prs/2023-04-26_TACAS23_Bridging_Hardware_and_Software_Analysis_with_Btor2C_Po-Chun.pdf}, abstract = {Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a converter from word-level sequential circuits to C programs. We choose <a href="https://doi.org/10.1007/978-3-319-96145-3_32">the Btor2 language</a> as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.}, keyword = {Software Model Checking, Cooperative Verification, Btor2}, _pdf = {https://www.sosy-lab.org/research/pub/2023-TACAS.Bridging_Hardware_and_Software_Analysis_with_Btor2C_A_Word-Level-Circuit-to-C_Translator.pdf}, artifact = {10.5281/zenodo.7551707}, funding = {DFG-CONVEY}, }
  11. Dirk Beyer, Jan Haltermann, Thomas Lemberger, and Heike Wehrheim. Component-based CEGAR - Building Software Verifiers from Off-the-Shelf Components. In G. Engels, R. Hebig, and M. Tichy, editors, Software Engineering 2023, Fachtagung des GI-Fachbereichs Softwaretechnik, 20.-24. Februar 2023, Paderborn, LNI P-332, pages 37-38, 2023. GI. Link to this entry Keyword(s): CPAchecker, Software Model Checking, Cooperative Verification Publisher's Version PDF
    BibTeX Entry
    @inproceedings{SE23, author = {Dirk Beyer and Jan Haltermann and Thomas Lemberger and Heike Wehrheim}, title = {Component-based {CEGAR} - Building Software Verifiers from Off-the-Shelf Components}, booktitle = {Software Engineering 2023, Fachtagung des GI-Fachbereichs Softwaretechnik, 20.-24. Februar 2023, Paderborn}, editor = {G.~Engels and R.~Hebig and M.~Tichy}, pages = {37--38}, year = {2023}, series = {{LNI}~P-332}, publisher = {{GI}}, sha256 = {}, pdf = {https://sosy-lab.org/research/pub/2023-SE.Component-based_CEGAR_Building_Software_Verifiers_from_Off-the-Shelf_Components.pdf}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Cooperative Verification}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2022.html#ICSE22">full article on this topic</a> that appeared in Proc. ICSE 2022.}, doinone = {DOI not available}, isbnnote = {978-3-88579-726-5}, urlpub = {https://dspace.gi.de/handle/20.500.12116/40128}, }
    Additional Infos
    This is a summary of a full article on this topic that appeared in Proc. ICSE 2022.
  12. Jan Haltermann, Marie-Christine Jakobs, Cedric Richter, and Heike Wehrheim. Parallel Program Analysis via Range Splitting. In Proc. FASE, LNCS 13991, pages 195-219, 2023. Springer. doi:10.1007/978-3-031-30826-0_11 Link to this entry Keyword(s): Ranged Program Analysis, Cooperative Verification, Software Model Checking, CPAchecker Funding: DFG-COOP Publisher's Version PDF
    BibTeX Entry
    @inproceedings{RangedPA-CPA, author = {Jan Haltermann and Marie{-}Christine Jakobs and Cedric Richter and Heike Wehrheim}, title = {Parallel Program Analysis via Range Splitting}, booktitle = {Proc.\ {FASE}}, pages = {195--219}, year = {2023}, series = {LNCS~13991}, publisher = {Springer}, doi = {10.1007/978-3-031-30826-0_11}, url = {}, pdf = {}, keyword = {Ranged Program Analysis, Cooperative Verification, Software Model Checking, CPAchecker}, annote = {}, artifact = {}, funding = {DFG-COOP}, }
  13. Dirk Beyer and Sudeep Kanav. CoVeriTeam: On-Demand Composition of Cooperative Verification Systems. In D. Fisman and G. Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7, LNCS 13243, pages 561-579, 2022. Springer. doi:10.1007/978-3-030-99524-9_31 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification Funding: DFG-COOP Publisher's Version PDF Presentation Supplement
    BibTeX Entry
    @inproceedings{TACAS22a, author = {Dirk Beyer and Sudeep Kanav}, title = {{CoVeriTeam}: {O}n-Demand Composition of Cooperative Verification Systems}, booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7}, editor = {D.~Fisman and G.~Rosu}, pages = {561-579}, year = {2022}, series = {LNCS~13243}, publisher = {Springer}, doi = {10.1007/978-3-030-99524-9_31}, sha256 = {e38311ae071351301b08d16849ee309a86efdc07fc45e18e466b4735ef21f241}, url = {https://www.sosy-lab.org/research/coveriteam/}, presentation = {https://www.sosy-lab.org/research/prs/2022-04-06_TACAS22_CoVeriTeam_Sudeep.pdf}, abstract = {}, keyword = {Software Model Checking,Cooperative Verification}, funding = {DFG-COOP}, }
  14. Dirk Beyer and Heike Wehrheim. Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework. In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodos, Greece, October 26-30), part 1, LNCS 12476, pages 143-167, 2020. Springer. doi:10.1007/978-3-030-61362-4_8 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification Funding: DFG-COOP Publisher's Version PDF Presentation
    BibTeX Entry
    @inproceedings{ISoLA20a, author = {Dirk Beyer and Heike Wehrheim}, title = {Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodos, Greece, October 26-30), part~1}, editor = {T.~Margaria and B.~Steffen}, pages = {143-167}, year = {2020}, series = {LNCS~12476}, publisher = {Springer}, doi = {10.1007/978-3-030-61362-4_8}, sha256 = {86dbfb5ee4875582566bdb5d44750cc935614c11c09627295cc3ff123115a75b}, url = {}, presentation = {https://www.sosy-lab.org/research/prs/2021-10-29_ISOLA21_VerificationArtifacts_Dirk.pdf}, abstract = {}, keyword = {Software Model Checking,Cooperative Verification}, funding = {DFG-COOP}, fundingid = {418257054}, }

Internal reports
  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 Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF Supplement
    Artifact(s)
    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.
  2. Po-Chun Chien. Bridging Hardware and Software Formal Verification (Extended Abstract). Technical report 2024-06, LMU Munich, 2024. Link to this entry Keyword(s): Software Model Checking, Cooperative Verification, Btor2, CPAchecker, Witness-Based Validation Funding: DFG-CONVEY PDF
    Abstract
    Modern technology relies heavily on the integration of hardware and software systems, from embedded devices in consumer electronics to safety-critical controllers. Despite their interdependence, the tools and methods used for verifying the correctness and reliability of these systems are often segregated, meaning that the advancement in one community cannot benefit another directly. Addressing this challenge, my dissertation aims at bridging the gap between hardware and software formal analysis. This involves translating representations of verification tasks, generating certificates for verification results, integrating state-of-the-art formal analysis tools into a cohesive framework, and adapting and combining model-checking algorithms across domains. By translating word-level hardware circuits into C programs, we found out that software analyzers were able to identify property violations that well-established hardware verifiers failed to detect. Moreover, by adopting interpolation-based hardware-verification algorithms for software analysis, we were able to tackle tasks unsolvable by existing methods. Our research consolidates knowledge from both hardware and software domains, paving a pathway for comprehensive system-level verification.
    BibTeX Entry
    @techreport{chien:fm24-doc-symposium, author = {Po-Chun Chien}, title = {Bridging Hardware and Software Formal Verification (Extended Abstract)}, number = {2024-06}, year = {2024}, pdf = {https://www.sosy-lab.org/research/pub/2024-FM_Doctoral_Symposium.Bridging_Hardware_and_Software_Formal_Verification_Extended_Abstract.pdf}, abstract = {Modern technology relies heavily on the integration of hardware and software systems, from embedded devices in consumer electronics to safety-critical controllers. Despite their interdependence, the tools and methods used for verifying the correctness and reliability of these systems are often segregated, meaning that the advancement in one community cannot benefit another directly. Addressing this challenge, my dissertation aims at bridging the gap between hardware and software formal analysis. This involves translating representations of verification tasks, generating certificates for verification results, integrating state-of-the-art formal analysis tools into a cohesive framework, and adapting and combining model-checking algorithms across domains. By translating word-level hardware circuits into C programs, we found out that software analyzers were able to identify property violations that well-established hardware verifiers failed to detect. Moreover, by adopting interpolation-based hardware-verification algorithms for software analysis, we were able to tackle tasks unsolvable by existing methods. Our research consolidates knowledge from both hardware and software domains, paving a pathway for comprehensive system-level verification.}, keyword = {Software Model Checking, Cooperative Verification, Btor2, CPAchecker, Witness-Based Validation}, annote = {An extended abstract of the dissertation project. Submitted to the Doctoral Symposium of FM 2024.}, funding = {DFG-CONVEY}, institution = {LMU Munich}, }
    Additional Infos
    An extended abstract of the dissertation project. Submitted to the Doctoral Symposium of FM 2024.

Theses and projects (PhD, MSc, BSc, Project)
  1. Thomas Lemberger. Towards Cooperative Software Verification with Test Generation and Formal Verification. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.32852 Link to this entry Keyword(s): CPAchecker, Software Model Checking, Cooperative Verification Publisher's Version PDF Presentation
    BibTeX Entry
    @misc{LembergerCoop, author = {Thomas Lemberger}, title = {Towards Cooperative Software Verification with Test Generation and Formal Verification}, year = {2022}, doi = {10.5282/edoc.32852}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/32852/1/Lemberger_Thomas.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-12-12_PhD_TowardsCooperativeSoftwareVerification_Thomas.pdf}, keyword = {CPAchecker,Software Model Checking,Cooperative Verification}, annote = {Nominated for the <a href="https://se2024.se.jku.at/ernst-denert-se-preis/">Ernst Denert SE-Preis 2024</a>}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-328522}, }
    Additional Infos
    Nominated for the Ernst Denert SE-Preis 2024

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: Mon Nov 18 19:35:54 2024 UTC