Software and Computational Systems Lab

Publications of Marie-Christine Jakobs

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 Keyword(s): Ranged Program Analysis, Cooperative Verification, Software Model Checking, CPAchecker Funding: DFG-COOP Publisher's Version
   Artifact(s)

   1. doi:10.5281/zenodo.8398988
   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. Marie-Christine Jakobs, Einar Broch Johnsen, Eduard Kamburjan, and Manuel Wimmer. Preface for the special issue on "Fundamental Approaches to Software Engineering" (FASE 2022). Science of Computer Programming, 232:103055, 2024. doi:10.1016/J.SCICO.2023.103055 Publisher's Version
   BibTeX Entry

   @article{FASE2022-SI, author = {Marie{-}Christine Jakobs and Einar Broch Johnsen and Eduard Kamburjan and Manuel Wimmer}, title = {Preface for the special issue on "Fundamental Approaches to Software Engineering" {(FASE} 2022)}, journal = {Science of Computer Programming}, volume = {232}, pages = {103055}, year = {2024}, doi = {10.1016/J.SCICO.2023.103055}, url = {}, pdf = {}, keyword = {}, annote = {}, artifact = {}, funding = {}, }
3. Marie-Christine Jakobs and Nian-Ze Lee. Summary of the Eighth International Workshop on CPAchecker (CPAchecker 2023). ACM SIGSOFT Software Engineering Notes, 49(2):25-26, 2024. doi:10.1145/3650142.3650150 Keyword(s): CPAchecker Publisher's Version PDF Supplement
   BibTeX Entry

   @article{CPAcheckerWorkshop, author = {Marie{-}Christine Jakobs and Nian{-}Ze Lee}, title = {Summary of the Eighth International Workshop on CPAchecker (CPAchecker 2023)}, journal = {{ACM} {SIGSOFT} Software Engineering Notes}, volume = {49}, number = {2}, pages = {25--26}, year = {2024}, doi = {10.1145/3650142.3650150}, url = {https://cpa.sosy-lab.org/2023/}, pdf = {}, keyword = {CPAchecker}, annote = {}, artifact = {}, funding = {}, }
4. Dirk Beyer and Marie-Christine Jakobs. Cooperative Verifier-Based Testing with CoVeriTest. International Journal on Software Tools for Technology Transfer (STTT), 23(3):313-333, 2021. doi:10.1007/s10009-020-00587-8 Keyword(s): CPAchecker, Software Model Checking, Software Testing Funding: DFG-COOP Publisher's Version PDF
   Abstract

   Testing is a widely applied technique to evaluate software quality, and coverage criteria are often used to assess the adequacy of a generated test suite. However, manually constructing an adequate test suite is typically too expensive, and numerous techniques for automatic test-suite generation were proposed. All of them come with different strengths. To build stronger test-generation tools, different techniques should be combined. In this paper, we study cooperative combinations of verification approaches for test generation, which exchange high-level information. We present CoVeriTest, a hybrid technique for test-suite generation. CoVeriTest iteratively applies different conditional model checkers and allows users to adjust the level of cooperation and to configure individual time limits for each conditional model checker. In our experiments, we systematically study different CoVeriTest cooperation setups, which either use combinations of explicit-state model checking and predicate abstraction, or bounded model checking and symbolic execution. A comparison with state-of-the-art test-generation tools reveals that CoVeriTest achieves higher coverage for many programs (about 15
   BibTeX Entry

   @article{CoVeriTest-STTT, author = {Dirk Beyer and Marie-Christine Jakobs}, title = {Cooperative Verifier-Based Testing with {CoVeriTest}}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {23}, number = {3}, pages = {313-333}, year = {2021}, doi = {10.1007/s10009-020-00587-8}, sha256 = {28a5bf6103296455728076e8c12902a53b3d377a296ea2ba18ac111c93330dbd}, url = {}, pdf = {}, presentation = {}, abstract = {Testing is a widely applied technique to evaluate software quality, and coverage criteria are often used to assess the adequacy of a generated test suite. However, manually constructing an adequate test suite is typically too expensive, and numerous techniques for automatic test-suite generation were proposed. All of them come with different strengths. To build stronger test-generation tools, different techniques should be combined. In this paper, we study cooperative combinations of verification approaches for test generation, which exchange high-level information. We present CoVeriTest, a hybrid technique for test-suite generation. CoVeriTest iteratively applies different conditional model checkers and allows users to adjust the level of cooperation and to configure individual time limits for each conditional model checker. In our experiments, we systematically study different CoVeriTest cooperation setups, which either use combinations of explicit-state model checking and predicate abstraction, or bounded model checking and symbolic execution. A comparison with state-of-the-art test-generation tools reveals that CoVeriTest achieves higher coverage for many programs (about 15%).}, keyword = {CPAchecker,Software Model Checking,Software Testing}, funding = {DFG-COOP}, issn = {1433-2787}, }
5. Marie-Christine Jakobs. Spontane Sicherheitsprüfung mittels individualisierter Programmzertifizierung oder Programmrestrukturierung. In S. Hölldobler, editors, Ausgezeichnete Informatikdissertationen 2017, LNI, pages 91-100, 2018. Gesellschaft für Informatik (GI). Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
   Abstract

   Korrekt funktionierende Software gewinnt immer mehr an Bedeutung. Im Vergleich zu früher ist es heutzutage schwieriger einzuschätzen, wie gut eine Software funktioniert. Dies liegt unter anderem daran, dass Endnutzer häufiger Software unbekannter Hersteller installieren. Endnutzer sollten sich also aktiv von der Softwarekorrektheit überzeugen, zum Beispiel in Form einer spontanen Sicherheitsprüfung. Übliche Verifikationstechniken zur Korrektheitsprüfung kommen für Endnutzer, in der Regel Laien, nicht in Frage. Die zentrale Frage ist daher, wie man einem Laien eine solche spontane Sicherheitsprüfung ermöglicht. Die Antwort der Dissertation sind einfache, automatische und generelle Verfahren zur Sicherheitsprüfung. In der Dissertation werden verschiedene Verfahren vorgeschlagen und sowohl theoretisch als auch praktisch untersucht. Die vorgeschlagenen Verfahren lassen sich in zwei Forschungsrichtungen einsortieren, nämlich in die Gruppe der Proof-Carrying Code Verfahren bzw. in die Gruppe des alternativen Programs from Proofs Verfahren. Einige Verfahren kombinieren beide Forschungsrichtungen.
   BibTeX Entry

   @incollection{DissZusammenfassungJakobs, author = {Marie-Christine Jakobs}, title = {Spontane Sicherheitspr{\"{u}}fung mittels individualisierter Programmzertifizierung oder Programmrestrukturierung}, booktitle = {Ausgezeichnete Informatikdissertationen 2017}, editor = {S. H{\"{o}}lldobler}, volume = {{D-18}}, pages = {91-100}, year = {2018}, series = {{LNI}}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, isbn = {978-3885799771}, pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/19486/invited_paper_14.pdf?sequence=1&isAllowed=y}, abstract = {Korrekt funktionierende Software gewinnt immer mehr an Bedeutung. Im Vergleich zu früher ist es heutzutage schwieriger einzuschätzen, wie gut eine Software funktioniert. Dies liegt unter anderem daran, dass Endnutzer häufiger Software unbekannter Hersteller installieren. Endnutzer sollten sich also aktiv von der Softwarekorrektheit überzeugen, zum Beispiel in Form einer spontanen Sicherheitsprüfung. Übliche Verifikationstechniken zur Korrektheitsprüfung kommen für Endnutzer, in der Regel Laien, nicht in Frage. Die zentrale Frage ist daher, wie man einem Laien eine solche spontane Sicherheitsprüfung ermöglicht. Die Antwort der Dissertation sind einfache, automatische und generelle Verfahren zur Sicherheitsprüfung. In der Dissertation werden verschiedene Verfahren vorgeschlagen und sowohl theoretisch als auch praktisch untersucht. Die vorgeschlagenen Verfahren lassen sich in zwei Forschungsrichtungen einsortieren, nämlich in die Gruppe der Proof-Carrying Code Verfahren bzw. in die Gruppe des alternativen Programs from Proofs Verfahren. Einige Verfahren kombinieren beide Forschungsrichtungen.}, keyword = {CPAchecker,Software Model Checking}, annote = {This is a German summary of the dissertation On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring.}, doifalse = {20.500.12116/19486}, urlpub = {https://dl.gi.de/handle/20.500.12116/19486}, }
   Additional Infos

   This is a German summary of the dissertation On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring.

6. Daniel Baier, Dirk Beyer, Po-Chun Chien, Marie-Christine Jakobs, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch-Rosenfeld, Henrik Wachowitz, and Philipp Wendler. Software Verification with CPAchecker 3.0: Tutorial and User Guide. In Proceedings of the 26th International Symposium on Formal Methods (FM 2024, Milan, Italy, September 9-13), LNCS 14934, pages 543-570, 2024. Springer. doi:10.1007/978-3-031-71177-0_30 Keyword(s): CPAchecker, Software Model Checking, Software Testing Funding: DFG-COOP, DFG-CONVEY, DFG-IDEFIX Publisher's Version PDF Presentation Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.13612338
   Abstract

   This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.
   BibTeX Entry

   @inproceedings{FM24a, author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marie-Christine Jakobs and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Henrik Wachowitz and Philipp Wendler}, title = {Software Verification with {CPAchecker} 3.0: {Tutorial} and User Guide}, booktitle = {Proceedings of the 26th International Symposium on Formal Methods (FM~2024, Milan, Italy, September 9-13)}, pages = {543-570}, year = {2024}, series = {LNCS~14934}, publisher = {Springer}, doi = {10.1007/978-3-031-71177-0_30}, url = {https://cpachecker.sosy-lab.org}, pdf = {https://www.sosy-lab.org/research/pub/2024-FM.Software_Verification_with_CPAchecker_3.0_Tutorial_and_User_Guide.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-09-10_FM24_CPAchecker_Tutorial.pdf}, abstract = {This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, <i>k</i>-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at <a href="https://cpachecker.sosy-lab.org/doc.php">https://cpachecker.sosy-lab.org/doc.php</a>.}, keyword = {CPAchecker, Software Model Checking, Software Testing}, annote = {An <a href="https://www.sosy-lab.org/research/bib/All/index.html#TechReport24c">extended version</a> of this article is available on <a href="https://doi.org/10.48550/arXiv.2409.02094">arXiv</a>.}, artifact = {10.5281/zenodo.13612338}, funding = {DFG-COOP, DFG-CONVEY, DFG-IDEFIX}, }
   Additional Infos

   An extended version of this article is available on arXiv.
7. Max Barth and Marie-Christine Jakobs. Refining CEGAR-based Test-Case Generation with Feasibility Annotations. In Proc. TAP , LNCS , 2024. Springer. Keyword(s): Ultimate Automizer, Software Testing Funding: DFG-ReVeriX
   Artifact(s)

   1. doi:10.5281/zenodo.11641893
   BibTeX Entry

   @inproceedings{UTestGen-Reuse, author = {Max Barth and Marie{-}Christine Jakobs}, title = {Refining CEGAR-based Test-Case Generation with Feasibility Annotations}, booktitle = {Proc.\ {TAP}}, pages = {}, year = {2024}, series = {LNCS~}, publisher = {Springer}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Testing}, annote = {}, artifact = {10.5281/zenodo.11641893}, doinone = {Unpublished: Last checked: 2024-07-08}, funding = {DFG-ReVeriX}, }
8. Max Barth and Marie-Christine Jakobs. Test-Case Generation with Automata-based Software Model Checking. In Proc. SPIN , LNCS , 2024. Springer. Keyword(s): Ultimate Automizer, Software Testing
   Artifact(s)

   1. doi:10.5281/zenodo.10574234
   BibTeX Entry

   @inproceedings{UTestGen, author = {Max Barth and Marie{-}Christine Jakobs}, title = {Test-Case Generation with Automata-based Software Model Checking}, booktitle = {Proc.\ {SPIN}}, pages = {}, year = {2024}, series = {LNCS~}, publisher = {Springer}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Testing}, annote = {}, artifact = {10.5281/zenodo.10574234}, doinone = {Unpublished: Last checked: 2024-07-08}, funding = {}, }
9. Max Barth, Daniel Dietsch, Matthias Heizmann, and Marie-Christine Jakobs. Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution). In Proc. FASE , LNCS 14573, pages 326-330, 2024. Springer. doi:10.1007/978-3-031-57259-3_20 Keyword(s): Ultimate Automizer, Software Testing Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.10071568
   BibTeX Entry

   @inproceedings{UTestGen-Competition, author = {Max Barth and Daniel Dietsch and Matthias Heizmann and Marie{-}Christine Jakobs}, title = {Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution)}, booktitle = {Proc.\ {FASE}}, pages = {326-330}, year = {2024}, series = {LNCS~14573}, publisher = {Springer}, doi = {10.1007/978-3-031-57259-3_20}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Testing}, annote = {}, artifact = {10.5281/zenodo.10071568}, funding = {}, }
10. 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 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 = {}, }
11. Marie-Christine Jakobs and Tim Pollandt. diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions. In Proc. iFM, LNCS 14300, pages 40-61, 2023. Springer. doi:10.1007/978-3-031-47705-8_3 Keyword(s): Incremental Verification, Regression Verification, Software Model Checking, CPAchecker Funding: Software-Factory 4.0, DFG-ReVeriX Publisher's Version PDF
    Artifact(s)

    1. doi:10.5281/zenodo.8272913
    BibTeX Entry

    @inproceedings{diffDP, author = {Marie{-}Christine Jakobs and Tim Pollandt}, title = {diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions}, booktitle = {Proc.\ iFM}, pages = {40-61}, year = {2023}, series = {LNCS~14300}, publisher = {Springer}, doi = {10.1007/978-3-031-47705-8_3}, url = {}, pdf = {}, keyword = {Incremental Verification, Regression Verification, Software Model Checking, CPAchecker}, annote = {}, artifact = {10.5281/zenodo.8272913}, funding = {Software-Factory 4.0, DFG-ReVeriX}, }
12. Jan Haltermann, Marie-Christine Jakobs, Cedric Richter, and Heike Wehrheim. Ranged Program Analysis via Instrumentation. In Proc. SEFM, LNCS 14323, pages 145-164, 2023. Springer. doi:10.1007/978-3-031-47115-5_9 Keyword(s): Software Model Checking, CPAchecker, Ranged Program Analysis, Program Instrumentation Publisher's Version PDF
    Artifact(s)

    1. doi:10.5281/zenodo.8065229
    BibTeX Entry

    @inproceedings{RangedPAwithInstrumentation, author = {Jan Haltermann and Marie{-}Christine Jakobs and Cedric Richter and Heike Wehrheim}, title = {Ranged Program Analysis via Instrumentation}, booktitle = {Proc.\ SEFM}, pages = {145-164}, year = {2023}, series = {LNCS~14323}, publisher = {Springer}, doi = {10.1007/978-3-031-47115-5_9}, url = {}, pdf = {}, keyword = {Software Model Checking, CPAchecker, Ranged Program Analysis, Program Instrumentation}, annote = {}, artifact = {10.5281/zenodo.8065229}, funding = {}, }
13. 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 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}, }
14. Cedric Richter, Jan Haltermann, Marie-Christine Jakobs, Felix Pauck, Stefan Schott, and Heike Wehrheim. Variable Misuse Detection: Software Developers versus Neural Bug Detectors. In Software Engineering 2023, Fachtagung des GI-Fachbereichs Softwaretechnik, 20.-24. Februar 2023, Paderborn, LNI P-332, pages 103-104, 2023. GI. Keyword(s): Bug Detection, Empirical Study Publisher's Version
    Artifact(s)

    1. doi:10.5281/zenodo.6958242
    BibTeX Entry

    @inproceedings{JakobsSE2023, author = {Cedric Richter and Jan Haltermann and Marie{-}Christine Jakobs and Felix Pauck and Stefan Schott and Heike Wehrheim}, title = {Variable Misuse Detection: Software Developers versus Neural Bug Detectors}, booktitle = {Software Engineering 2023, Fachtagung des GI-Fachbereichs Softwaretechnik, 20.-24. Februar 2023, Paderborn}, pages = {103-104}, year = {2023}, series = {{LNI}~{P-332}}, publisher = {GI}, pdf = {}, keyword = {Bug Detection, Empirical Study}, artifact = {10.5281/zenodo.6958242}, doinone = {DOI not available}, urlpub = {https://dl.gi.de/handle/20.500.12116/40105}, }
15. Dirk Beyer, Marie-Christine Jakobs, and Thomas Lemberger. Difference Verification with Conditions. In F. d. Boer and A. Cerone, editors, Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM 2020, Virtual, Netherlands, September 14-18), LNCS 12310, pages 133-154, 2020. Springer. doi:10.1007/978-3-030-58768-0_8 Keyword(s): CPAchecker, Software Model Checking Funding: DFG-COOP, DFG-CONVEY Publisher's Version PDF Presentation Video Supplement
    Abstract

    Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.
    BibTeX Entry

    @inproceedings{SEFM20b, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger}, title = {Difference Verification with Conditions}, booktitle = {Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18)}, editor = {F.~d.~Boer and A.~Cerone}, pages = {133--154}, year = {2020}, series = {LNCS~12310}, publisher = {Springer}, doi = {10.1007/978-3-030-58768-0_8}, sha256 = {8e5219da9a998b26f59013c809fbb1db6f92e3f08125fa1bfaacafcfafafef7f}, url = {https://www.sosy-lab.org/research/difference/}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-17_SEFM20_DifferenceVerificationWithConditions_Thomas.pdf}, abstract = {Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.}, keyword = {CPAchecker,Software Model Checking}, funding = {DFG-COOP,DFG-CONVEY}, isbnnote = {}, video = {https://youtu.be/dG02602c9oo}, }
16. Dirk Beyer and Marie-Christine Jakobs. FRed: Conditional Model Checking via Reducers and Folders. In F. d. Boer and A. Cerone, editors, Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM 2020, Virtual, Netherlands, September 14-18), LNCS 12310, pages 113-132, 2020. Springer. doi:10.1007/978-3-030-58768-0_7 Keyword(s): CPAchecker, Software Model Checking Funding: DFG-COOP Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{SEFM20a, author = {Dirk Beyer and Marie-Christine Jakobs}, title = {{{\sc FRed}}: {C}onditional Model Checking via Reducers and Folders}, booktitle = {Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18)}, editor = {F.~d.~Boer and A.~Cerone}, pages = {113--132}, year = {2020}, series = {LNCS~12310}, publisher = {Springer}, doi = {10.1007/978-3-030-58768-0_7}, sha256 = {0ce35cbde24d7a9de0513b89f23a81147bf4f8d5880effd57742c7f195e0eeec}, url = {https://www.sosy-lab.org/research/fred/}, abstract = {}, keyword = {CPAchecker,Software Model Checking}, funding = {DFG-COOP}, isbnnote = {}, }
17. Dirk Beyer and Marie-Christine Jakobs. Cooperative Test-Case Generation with Verifiers. In M. Felderer, W. Hasselbring, R. Rabiser, and R. Jung, editors, Proceedings of the Conference on Software Engineering (SE 2020, Innsbruck, Austria, February 24-28), LNI P-300, pages 107-108, 2020. GI. doi:10.18420/SE2020_31 Keyword(s): CPAchecker, Software Model Checking, Software Testing Publisher's Version
    BibTeX Entry

    @inproceedings{SE20, author = {Dirk Beyer and Marie-Christine Jakobs}, title = {Cooperative Test-Case Generation with Verifiers}, booktitle = {Proceedings of the Conference on Software Engineering (SE~2020, Innsbruck, Austria, February 24-28)}, editor = {M.~Felderer and W.~Hasselbring and R.~Rabiser and R.~Jung}, pages = {107--108}, year = {2020}, series = {{LNI}~P-300}, publisher = {{GI}}, doi = {10.18420/SE2020_31}, sha256 = {}, pdf = {}, presentation = {}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Software Testing}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2019.html#FASE19">full article on this topic</a> that appeared in Proc. FASE 2019.}, isbnnote = {978-3-88579-694-7}, }
    Additional Infos

    This is a summary of a full article on this topic that appeared in Proc. FASE 2019.
18. Dirk Beyer and Marie-Christine Jakobs. CoVeriTest: Cooperative Verifier-Based Testing. In Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE 2019, Prague, Czech Republic, April 6-11), LNCS 11424, pages 389-408, 2019. Springer. doi:10.1007/978-3-030-16722-6_23 Keyword(s): CPAchecker, Software Model Checking, Software Testing Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{FASE19, author = {Dirk Beyer and Marie-Christine Jakobs}, title = {CoVeriTest: Cooperative Verifier-Based Testing}, booktitle = {Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE~2019, Prague, Czech Republic, April 6-11)}, pages = {389-408}, year = {2019}, series = {LNCS~11424}, publisher = {Springer}, doi = {10.1007/978-3-030-16722-6_23}, sha256 = {ee64749fba4796ed79cecfaa500731ef2ac5d5e795770c44b1e7ad358f955398}, url = {https://www.sosy-lab.org/research/coop-testgen/}, keyword = {CPAchecker,Software Model Checking,Software Testing}, }
19. Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim. Combining Verifiers in Conditional Model Checking via Reducers. In S. Becker, I. Bogicevic, G. Herzwurm, and S. Wagner, editors, Proceedings of the Conference on Software Engineering and Software Management (SE/SWM 2019, Stuttgart, Germany, February 18-22), LNI P-292, pages 151-152, 2019. GI. doi:10.18420/se2019-46 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation
    Abstract

    Software verification received lots of attention in the past two decades. Nonetheless, it remains an extremely difficult problem. Some verification tasks cannot be solved automatically by any of today’s verifiers. To still verify such tasks, one can combine the strengths of different verifiers. A promising approach to create combinations is conditional model checking (CMC). In CMC, the first verifier outputs a condition that describes the parts of the program state space that it successfully verified, and the next verifier uses that condition to steer its exploration towards the unverified state space. Despite the benefits of CMC, only few verifiers can handle conditions. To overcome this problem, we propose an automatic plug-and-play extension for verifiers. Instead of modifying verifiers, we suggest to add a preprocessor: the reducer. The reducer takes the condition and the original program and computes a residual program that encodes the unverified state space in program code. We developed one such reducer and use it to integrate existing verifiers and test-case generators into the CMC process. Our experiments show that we can solve many additional verification tasks with this reducer-based construction.
    BibTeX Entry

    @inproceedings{SE19, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger and Heike Wehrheim}, title = {Combining Verifiers in Conditional Model Checking via Reducers}, booktitle = {Proceedings of the Conference on Software Engineering and Software Management (SE/SWM~2019, Stuttgart, Germany, February 18-22)}, editor = {S.~Becker and I.~Bogicevic and G.~Herzwurm and S.~Wagner}, pages = {151--152}, year = {2019}, series = {{LNI}~P-292}, publisher = {{GI}}, doi = {10.18420/se2019-46}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2019-SE.Combining_Verifiers_in_Conditional_Model_Checking_via_Reducers.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-02-22_SE19_CombiningVerifiersInConditionalModelChecking_Marie.pdf}, abstract = {Software verification received lots of attention in the past two decades. Nonetheless, it remains an extremely difficult problem. Some verification tasks cannot be solved automatically by any of today’s verifiers. To still verify such tasks, one can combine the strengths of different verifiers. A promising approach to create combinations is conditional model checking (CMC). In CMC, the first verifier outputs a condition that describes the parts of the program state space that it successfully verified, and the next verifier uses that condition to steer its exploration towards the unverified state space. Despite the benefits of CMC, only few verifiers can handle conditions. To overcome this problem, we propose an automatic plug-and-play extension for verifiers. Instead of modifying verifiers, we suggest to add a preprocessor: the reducer. The reducer takes the condition and the original program and computes a residual program that encodes the unverified state space in program code. We developed one such reducer and use it to integrate existing verifiers and test-case generators into the CMC process. Our experiments show that we can solve many additional verification tasks with this reducer-based construction.}, keyword = {CPAchecker,Software Model Checking}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2018.html#ICSE18">full article on this topic</a> that appeared in Proc. ICSE 2018.}, }
    Additional Infos

    This is a summary of a full article on this topic that appeared in Proc. ICSE 2018.
20. Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim. Reducer-Based Construction of Conditional Verifiers. In Proceedings of the 40th International Conference on Software Engineering (ICSE 2018, Gothenburg, Sweden, May 27 - June 3), pages 1182-1193, 2018. ACM. doi:10.1145/3180155.3180259 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
    Abstract

    Despite recent advances, software verification remains challenging. To solve hard verification tasks, we need to leverage not just one but several different verifiers employing different technologies. To this end, we need to exchange information between verifiers. Conditional model checking was proposed as a solution to exactly this problem: The idea is to let the first verifier output a condition which describes the state space that it successfully verified and to instruct the second verifier to verify the yet unverified state space using this condition. However, most verifiers do not understand conditions as input. In this paper, we propose the usage of an off-the-shelf construction of a conditional verifier from a given traditional verifier and a reducer. The reducer takes as input the program to be verified and the condition, and outputs a residual program whose paths cover the unverified state space described by the condition. As a proof of concept, we designed and implemented one particular reducer and composed three conditional model checkers from the three best verifiers at SV-COMP 2017. We defined a set of claims and experimentally evaluated their validity. All experimental data and results are available for replication.
    BibTeX Entry

    @inproceedings{ICSE18, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger and Heike Wehrheim}, title = {Reducer-Based Construction of Conditional Verifiers}, booktitle = {Proceedings of the 40th International Conference on Software Engineering (ICSE~2018, Gothenburg, Sweden, May 27 - June 3)}, pages = {1182-1193}, year = {2018}, publisher = {ACM}, isbn = {978-1-4503-5638-1}, doi = {10.1145/3180155.3180259}, sha256 = {}, url = {https://www.sosy-lab.org/research/reducer/}, pdf = {https://www.sosy-lab.org/research/pub/2018-ICSE.Reducer-Based_Construction_of_Conditional_Verifiers.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-06-01_ICSE18_ReducerBasedConstructionOfConditionalVerifiers_Marie.pdf}, abstract = {Despite recent advances, software verification remains challenging. To solve hard verification tasks, we need to leverage not just one but several different verifiers employing different technologies. To this end, we need to exchange information between verifiers. Conditional model checking was proposed as a solution to exactly this problem: The idea is to let the first verifier output a condition which describes the state space that it successfully verified and to instruct the second verifier to verify the yet unverified state space using this condition. However, most verifiers do not understand conditions as input. In this paper, we propose the usage of an off-the-shelf construction of a conditional verifier from a given traditional verifier and a reducer. The reducer takes as input the program to be verified and the condition, and outputs a residual program whose paths cover the unverified state space described by the condition. As a proof of concept, we designed and implemented one particular reducer and composed three conditional model checkers from the three best verifiers at SV-COMP 2017. We defined a set of claims and experimentally evaluated their validity. All experimental data and results are available for replication.}, keyword = {CPAchecker,Software Model Checking}, }

21. Daniel Baier, Dirk Beyer, Po-Chun Chien, Marie-Christine Jakobs, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch-Rosenfeld, Henrik Wachowitz, and Philipp Wendler. Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version). Technical report 2409.02094, arXiv/CoRR, September 2024. doi:10.48550/arXiv.2409.02094 Keyword(s): CPAchecker, Software Model Checking, Software Testing Funding: DFG-COOP, DFG-CONVEY, DFG-IDEFIX Publisher's Version PDF Presentation Supplement
    Artifact(s)

    1. doi:10.5281/zenodo.13612338
    Abstract

    This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.
    BibTeX Entry

    @techreport{TechReport24c, author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marie-Christine Jakobs and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Henrik Wachowitz and Philipp Wendler}, title = {Software Verification with {CPAchecker} 3.0: {Tutorial} and User Guide (Extended Version)}, number = {2409.02094}, year = {2024}, doi = {10.48550/arXiv.2409.02094}, url = {https://cpachecker.sosy-lab.org}, presentation = {https://www.sosy-lab.org/research/prs/2024-09-10_FM24_CPAchecker_Tutorial.pdf}, abstract = {This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, <i>k</i>-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at <a href="https://cpachecker.sosy-lab.org/doc.php">https://cpachecker.sosy-lab.org/doc.php</a>.}, keyword = {CPAchecker, Software Model Checking, Software Testing}, annote = {This technical report is an extended version of our <a href="https://www.sosy-lab.org/research/bib/All/index.html#FM24a">paper</a> at FM 2024.}, artifact = {10.5281/zenodo.13612338}, funding = {DFG-COOP, DFG-CONVEY, DFG-IDEFIX}, institution = {arXiv/CoRR}, month = {September}, }
    Additional Infos

    This technical report is an extended version of our paper at FM 2024.
22. Marie-Christine Jakobs and Tim Pollandt. Incorporating Data Dependencies and Properties in Difference Verification with Conditions (Technical Report). Technical report 2309.01585, arXiv/CoRR, 2023. doi:10.48550/arXiv.2309.01585 Keyword(s): Incremental Verification, Regression Verification, Software Model Checking, CPAchecker Funding: Software-Factory 4.0, DFG-ReVeriX Publisher's Version PDF
    Artifact(s)

    1. doi:10.5281/zenodo.8272913
    BibTeX Entry

    @techreport{diffDP-TechReport, author = {Marie{-}Christine Jakobs and Tim Pollandt}, title = {Incorporating Data Dependencies and Properties in Difference Verification with Conditions (Technical Report)}, number = {2309.01585}, year = {2023}, doi = {10.48550/arXiv.2309.01585}, url = {}, pdf = {}, keyword = {Incremental Verification, Regression Verification, Software Model Checking, CPAchecker}, annote = {This technical report is an extended version of our <a href="https://www.sosy-lab.org/research/bib/All/index.html#diffDP">paper</a> at iFM 2023.}, artifact = {10.5281/zenodo.8272913}, funding = {Software-Factory 4.0, DFG-ReVeriX}, institution = {arXiv/CoRR}, }
    Additional Infos

    This technical report is an extended version of our paper at iFM 2023.