Publications of year 2024
Books and proceedings
-
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}, }
Articles in journal or book chapters
-
Six Years Later: Testing vs. Model Checking.
International Journal on Software Tools for Technology Transfer (STTT),
2024.
Keyword(s):
Benchmarking,
Competition on Software Verification (SV-COMP),
Competition on Software Testing (Test-Comp),
Software Model Checking,
Software Testing
Funding:
DFG-COOP
PDF
Artifact(s)
Abstract
Six years ago, we performed the first large-scale comparison of automated test generators and software model checkers with respect to bug-finding capabilities on a benchmark set with 5 693 C programs. Since then, the International Competition on Software Testing (Test-Comp) has established standardized formats and community-agreed rules for the experimental comparison of test generators. With this new context, it is time to revisit our initial question: Model checkers or test generators—which tools are more effective in finding bugs in software? To answer this, we perform a comparative analysis on the tools and existing data published by two competitions, the International Competition on Software Verification (SV-COMP) and Test-Comp. The results provide two insights: (1) Almost all test generators that participate in Test-Comp use hybrid approaches that include formal methods, and (2) while the considered model checkers are still highly competitive, they are now outperformed by the bug-finding capabilities of the considered test generators.BibTeX Entry
@article{TestStudy-STTT, author = {Dirk Beyer and Thomas Lemberger}, title = {Six Years Later: Testing vs. Model Checking}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {}, number = {}, pages = {}, year = {2024}, doi = {}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2024-STTT.Six_Years_Later_Testing_vs_Model_Checking.pdf}, presentation = {}, abstract = {Six years ago, we performed the first large-scale comparison of automated test generators and software model checkers with respect to bug-finding capabilities on a benchmark set with 5 693 C programs. Since then, the International Competition on Software Testing (Test-Comp) has established standardized formats and community-agreed rules for the experimental comparison of test generators. With this new context, it is time to revisit our initial question: Model checkers or test generators—which tools are more effective in finding bugs in software? To answer this, we perform a comparative analysis on the tools and existing data published by two competitions, the International Competition on Software Verification (SV-COMP) and Test-Comp. The results provide two insights: (1) Almost all test generators that participate in Test-Comp use hybrid approaches that include formal methods, and (2) while the considered model checkers are still highly competitive, they are now outperformed by the bug-finding capabilities of the considered test generators.}, keyword = {Benchmarking, Competition on Software Verification (SV-COMP), Competition on Software Testing (Test-Comp), Software Model Checking, Software Testing}, artifact = {10.5281/zenodo.10232648}, funding = {DFG-COOP}, } -
A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification.
Proc. ACM Softw. Eng., 1(FSE),
2024.
ACM.
doi:10.1145/3660797
Keyword(s):
CPAchecker,
Software Model Checking
Funding:
DFG-CONVEY
Publisher's Version
PDF
Presentation
Supplement
Artifact(s)
Abstract
Assuring the correctness of computing systems is fundamental to our society and economy, and formal verification is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades, Craig interpolation has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking, (1) Interpolation-Sequence-Based Model Checking (Vizel and Grumberg, 2009) and (2) Intertwined Forward-Backward Reachability Analysis Using Interpolants (Vizel, Grumberg, and Shoham, 2013), for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks for the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware and software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms.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 for Software Verification}, journal = {Proc. ACM Softw. Eng.}, volume = {1}, number = {FSE}, year = {2024}, publisher = {ACM}, doi = {10.1145/3660797}, url = {https://www.sosy-lab.org/research/dar-ismc-transferability/}, presentation = {https://www.sosy-lab.org/research/prs/2024-07-18_FSE_A_Transferability_Study_of_Interpolation-Based_HWMC_for_SV_Marek.pdf}, abstract = {Assuring the correctness of computing systems is fundamental to our society and economy, and <em>formal verification</em> is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades, <em>Craig interpolation</em> has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking, (1) <em>Interpolation-Sequence-Based Model Checking</em> (<a href="https://doi.org/10.1109/FMCAD.2009.5351148">Vizel and Grumberg, 2009</a>) and (2) <em>Intertwined Forward-Backward Reachability Analysis Using Interpolants</em> (<a href="https://doi.org/10.1007/978-3-642-36742-7_22">Vizel, Grumberg, and Shoham, 2013</a>), for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks for the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware and software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms.}, keyword = {CPAchecker,Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2024-FSE.A_Transferability_Study_of_Interpolation-Based_Hardware_Model_Checking_for_Software_Verification.pdf}, annote = {This article received the "ACM SIGSOFT Distinguished Paper Award" and its reproduction artifact received the "ACM SIGSOFT Best Artifact Award" at <a href="https://2024.esec-fse.org/info/awards">FSE 2024</a>!}, articleno = {90}, artifact = {10.5281/zenodo.11070973}, funding = {DFG-CONVEY}, issue_date = {July 2024}, numpages = {23}, }Additional Infos
This article received the "ACM SIGSOFT Distinguished Paper Award" and its reproduction artifact received the "ACM SIGSOFT Best Artifact Award" at FSE 2024! -
Decomposing Software Verification using Distributed Summary Synthesis.
Proc. ACM Softw. Eng., 1(FSE),
2024.
ACM.
doi:10.1145/3660766
Keyword(s):
CPAchecker,
Software Model Checking
Funding:
DFG-CONVEY,
DFG-COOP
Publisher's Version
PDF
Supplement
Artifact(s)
Abstract
There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries are computed — based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (which program states reach this block) and verification conditions to check at the block exit (which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a precondition or verification condition) is available from other blocks, the verification can decide to restart with this new information. We realize our approach as an extension of the configurable-program-analysis algorithm and implement it for the verification of C programs in the widely used verifier CPAchecker. A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.BibTeX Entry
@article{DSS-PACMSE, author = {Dirk Beyer and Matthias Kettl and Thomas Lemberger}, title = {Decomposing Software Verification using Distributed Summary Synthesis}, journal = {Proc. ACM Softw. Eng.}, volume = {1}, number = {FSE}, year = {2024}, publisher = {ACM}, doi = {10.1145/3660766}, url = {https://www.sosy-lab.org/research/distributed-summary-synthesis/}, presentation = {}, abstract = {There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries are computed — based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (which program states reach this block) and verification conditions to check at the block exit (which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a precondition or verification condition) is available from other blocks, the verification can decide to restart with this new information. We realize our approach as an extension of the configurable-program-analysis algorithm and implement it for the verification of C programs in the widely used verifier CPAchecker. A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.}, keyword = {CPAchecker,Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2024-FSE.Decomposing_Software_Verification_using_Distributed_Summary_Synthesis.pdf}, articleno = {90}, artifact = {10.5281/zenodo.11095864}, funding = {DFG-CONVEY,DFG-COOP}, issue_date = {July 2024}, numpages = {23}, } -
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 = {}, } -
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)
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}, } -
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 = {}, } -
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 = {}, } -
Cooperative Approaches Across Test Generation and Formal Software Verification.
Softwaretechnik-Trends, 44(2):66-67,
July
2024.
Gesellschaft für Informatik, Berlin.
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
-
BenchCloud: A Platform for Scalable Performance Benchmarking.
In Proc. ASE,
2024.
ACM.
doi:10.1145/3691620.3695358
Keyword(s):
Benchmarking,
Competition on Software Verification (SV-COMP),
Competition on Software Testing (Test-Comp)
Funding:
DFG-CONVEY,
DFG-COOP
Publisher's Version
PDF
Video
Supplement
Artifact(s)
Abstract
Performance evaluation is a crucial method for assessing automated-reasoning tools. Evaluating automated tools requires rigorous benchmarking to accurately measure resource consumption, including time and memory, which are essential for understanding the tools' capabilities. BenchExec, a widely used benchmarking framework, reliably measures resource usage for tools executed locally on a single node. This paper describes BenchCloud, a solution for elastic and scalable job distribution across hundreds of nodes, enabling large-scale experiments on distributed and heterogeneous computing environments. BenchCloud seamlessly integrates with BenchExec, allowing BenchExec to delegate the actual execution to BenchCloud. The system has been employed in several prominent international competitions in automated reasoning, including SMT-COMP, SV-COMP, and Test-Comp, underscoring its importance in rigorous tool evaluation across various research domains. It helps to ensure both internal and external validity of the experimental results. This paper presents an overview of BenchCloud's architecture and high- lights its primary use cases in facilitating scalable benchmarking.
Demonstration video: https://youtu.be/aBfQytqPm0U
Running system: https://benchcloud.sosy-lab.org/BibTeX Entry
@inproceedings{ASE24a, author = {Dirk Beyer and Po-Chun Chien and Marek Jankola}, title = {{BenchCloud}: {A} Platform for Scalable Performance Benchmarking}, booktitle = {Proc.\ ASE}, pages = {}, year = {2024}, series = {}, publisher = {ACM}, doi = {10.1145/3691620.3695358}, url = {https://benchcloud.sosy-lab.org/}, pdf = {https://www.sosy-lab.org/research/pub/2024-ASE24.BenchCloud_A_Platform_for_Scalable_Performance_Benchmarking.pdf}, presentation = {}, abstract = {Performance evaluation is a crucial method for assessing automated-reasoning tools. Evaluating automated tools requires rigorous benchmarking to accurately measure resource consumption, including time and memory, which are essential for understanding the tools' capabilities. BenchExec, a widely used benchmarking framework, reliably measures resource usage for tools executed locally on a single node. This paper describes BenchCloud, a solution for elastic and scalable job distribution across hundreds of nodes, enabling large-scale experiments on distributed and heterogeneous computing environments. BenchCloud seamlessly integrates with BenchExec, allowing BenchExec to delegate the actual execution to BenchCloud. The system has been employed in several prominent international competitions in automated reasoning, including SMT-COMP, SV-COMP, and Test-Comp, underscoring its importance in rigorous tool evaluation across various research domains. It helps to ensure both internal and external validity of the experimental results. This paper presents an overview of BenchCloud's architecture and high- lights its primary use cases in facilitating scalable benchmarking. <br> Demonstration video: <a href="https://youtu.be/aBfQytqPm0U">https://youtu.be/aBfQytqPm0U</a> <br> Running system: <a href="https://benchcloud.sosy-lab.org/">https://benchcloud.sosy-lab.org/</a>}, keyword = {Benchmarking, Competition on Software Verification (SV-COMP), Competition on Software Testing (Test-Comp)}, artifact = {10.5281/zenodo.13742756}, funding = {DFG-CONVEY, DFG-COOP}, video = {https://youtu.be/aBfQytqPm0U}, } -
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.
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}, } -
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)
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. -
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)
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}, } -
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
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. -
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 14624,
pages 205-224,
2024.
Springer.
doi:10.1007/978-3-031-66149-5_12
Keyword(s):
Software Model Checking,
Witness-Based Validation,
CPAchecker
Funding:
DFG-CONVEY,
DFG-IDEFIX,
DFG-COOP
Publisher's Version
PDF
Artifact(s)
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{SPIN24b, 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 = {205-224}, year = {2024}, series = {LNCS~14624}, publisher = {Springer}, doi = {10.1007/978-3-031-66149-5_12}, 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}, 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. -
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
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}, } -
CPAchecker 2.3 with Strategy Selection (Competition Contribution).
In 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 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)
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 = {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}, 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/}, 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}, _pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.CPAchecker_2.3_with_Strategy_Selection_Competition_Contribution.pdf}, artifact = {10.5281/zenodo.10203297}, funding = {DFG-CONVEY, DFG-IDEFIX}, } -
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/}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.State_of_the_Art_in_Software_Verification_and_Witness_Validation_SV-COMP_2024.pdf}, funding = {DFG-CONVEY}, } -
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)
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% 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! -
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)
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}, } -
Test-Case Generation with
Automata-based Software Model Checking.
In Proc. SPIN ,
LNCS ,
2024.
Springer.
Keyword(s):
Ultimate Automizer,
Software Testing
Artifact(s)
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 = {}, } -
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)
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 = {}, } -
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 = {}, } -
Regression-Test History Data for Flaky Test Research.
In Proc. 1st International Workshop on Flaky Tests,
pages 3–4,
2024.
ACM.
doi:10.1145/3643656.3643901
Keyword(s):
Software Testing,
Flaky Tests
Publisher's Version
PDF
Presentation
Artifact(s)
Abstract
Due to their random nature, flaky test failures are difficult to study. Without having observed a test to both pass and fail under the same setup, it is unknown whether a test is flaky and what its failure rate is. Thus, flaky-test research has greatly benefited from data records of previous studies, which provide evidence for flaky test failures and give a rough indication of the failure rates to expect. For assessing the impact of the studied flaky tests on developers' work, it is important to also know how flaky test failures manifest over a regression test history, i.e., under continuous changes to test code or code under test. While existing datasets on flaky tests are mostly based on re-runs on an invariant code base, the actual effects of flaky tests on development can only be assessed across the commits in an evolving commit history, against which (potentially flaky) regression tests are executed. In our presentation, we outline approaches to bridge this gap and report on our experiences following one of them. As a result of this work, we contribute a dataset of flaky test failures across a simulated regression test history.BibTeX Entry
@inproceedings{RegressionTestData-FTW24, author = {Philipp Wendler and Stefan Winter}, title = {Regression-Test History Data for Flaky Test Research}, booktitle = {Proc.\ 1st International Workshop on Flaky Tests}, pages = {3–4}, year = {2024}, publisher = {ACM}, doi = {10.1145/3643656.3643901}, pdf = {https://www.sosy-lab.org/research/pub/2024-FTW24.Regression-Test_History_Data_for_Flaky_Test_Research.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-14_FTW24_Regression-Test_History_Data_for_Flaky_Test_Research_Stefan.html}, abstract = {Due to their random nature, flaky test failures are difficult to study. Without having observed a test to both pass and fail under the same setup, it is unknown whether a test is flaky and what its failure rate is. Thus, flaky-test research has greatly benefited from data records of previous studies, which provide evidence for flaky test failures and give a rough indication of the failure rates to expect. For assessing the impact of the studied flaky tests on developers' work, it is important to also know how flaky test failures manifest over a regression test history, i.e., under continuous changes to test code or code under test. While existing datasets on flaky tests are mostly based on re-runs on an invariant code base, the actual effects of flaky tests on development can only be assessed across the commits in an evolving commit history, against which (potentially flaky) regression tests are executed. In our presentation, we outline approaches to bridge this gap and report on our experiences following one of them. As a result of this work, we contribute a dataset of flaky test failures across a simulated regression test history.}, keyword = {Software Testing, Flaky Tests}, artifact = {10.5281/zenodo.10639030}, keywords = {Software Testing, Dataset}, } -
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
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/oZoOARuIOuABibTeX 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}, } -
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)
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}, } -
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}, }
Internal reports
-
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)
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. -
MoXIchecker: An Extensible Model Checker for MoXI.
Technical report 2407.15551, arXiv/CoRR,
March
2024.
doi:10.48550/arXiv.2407.15551
Keyword(s):
Btor2
Funding:
DFG-CONVEY,
DFG-BRIDGE
Publisher's Version
PDF
Supplement
Artifact(s)
Abstract
MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB 2 language with constructs to define state-transition systems. The tool suite of MoXI provides a translator from MoXI to Btor2, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for Btor2 to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in Btor2. We present MoXIchecker, the first model checker that solves MoXI verification tasks directly. Instead of translating MoXI to lower-level languages, MoXIchecker uses the solver-agnostic library PySMT for SMT solvers as backend for its verification algorithms. MoXIchecker is extensible because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the MoXI tool suite.BibTeX Entry
@techreport{TechReport24b, author = {Salih Ates and Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {{MoXIchecker}: {An} Extensible Model Checker for {MoXI}}, number = {2407.15551}, year = {2024}, doi = {10.48550/arXiv.2407.15551}, url = {https://gitlab.com/sosy-lab/software/moxichecker}, pdf = {https://arxiv.org/abs/2407.15551}, abstract = {MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB 2 language with constructs to define state-transition systems. The tool suite of MoXI provides a translator from MoXI to Btor2, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for Btor2 to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in Btor2. We present MoXIchecker, the first model checker that solves MoXI verification tasks directly. Instead of translating MoXI to lower-level languages, MoXIchecker uses the solver-agnostic library PySMT for SMT solvers as backend for its verification algorithms. MoXIchecker is extensible because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the MoXI tool suite.}, keyword = {Btor2}, artifact = {10.5281/zenodo.12787654}, funding = {DFG-CONVEY,DFG-BRIDGE}, institution = {arXiv/CoRR}, month = {March}, } -
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)
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. -
Bridging Hardware and Software Formal Verification (Extended Abstract).
Technical report 2024-06, LMU Munich,
2024.
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)
-
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}, } -
Creating an Exchangeable Intermediate Program Representation for the Formal Software Verifier CPAchecker.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
CPAchecker
BibTeX Entry
@misc{LindenmeierCfaJsonExport, author = {Felix Lindenmeier}, title = {Creating an Exchangeable Intermediate Program Representation for the Formal Software Verifier CPAchecker}, year = {2024}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Streamlining Software Verification: A Maven Plugin for Formal Verification of Java Code.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
Software Model Checking
PDF
BibTeX Entry
@misc{MartinJbmcMavenPlugin, author = {Yannick Martin}, title = {Streamlining Software Verification: A Maven Plugin for Formal Verification of Java Code}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Martin.Streamlining_Software_Verification_A_Maven_Plugin_for_Formal_Verification_of_Java_Code.pdf}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
From Compilation to Verification: Extending Gradle with JBMC for Enhanced Code Safety.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
Software Model Checking
BibTeX Entry
@misc{DubchakJbmcGradlePlugin, author = {Ella Dubchak}, title = {From Compilation to Verification: Extending Gradle with JBMC for Enhanced Code Safety}, year = {2024}, keyword = {Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Evaluation of JVM Garbage Collectors for CPAchecker.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
CPAchecker,
Benchmarking
PDF
Presentation
BibTeX Entry
@misc{MagetEvaluationJVMGarbageCollectorsCPAchecker, author = {Tobias Maget}, title = {Evaluation of JVM Garbage Collectors for CPAchecker}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Maget.Evaluation_of_JVM_Garbage_Collectors_for_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-10-23-BA_Evaluation_of_JVM_Garbage_Collectors_for_CPAchecker_Maget.pdf}, keyword = {CPAchecker, Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Witness Modifications for Program Transformations: A Case Study on Side-Effect Removal.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
Keyword(s):
Witnesses
PDF
BibTeX Entry
@misc{OvezovaWitnessModificationsSideEffectsCaseStudy, author = {Anna Ovezova}, title = {Witness Modifications for Program Transformations: A Case Study on Side-Effect Removal}, year = {2024}, pdf = {https://www.sosy-lab.org/research/bsc/2024.Ovezova.Witness_Modifications_for_Program_Transformations_A_Case_study_on_Side-Effect_Removal.pdf}, keyword = {Witnesses}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
Auswahl des Testalgorithmus mittels boolescher Merkmale.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
BibTeX Entry
@misc{TestAlgorithmSelection, author = {Khrystyna Reichel}, title = {Auswahl des Testalgorithmus mittels boolescher Merkmale}, year = {2024}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, } -
Auswahl der Zeitlimits für CoVeriTest mittels boolescher Merkmale.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2024.
BibTeX Entry
@misc{TestTimeSelection, author = {Iurii Irkha}, title = {Auswahl der Zeitlimits für CoVeriTest mittels boolescher Merkmale}, year = {2024}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
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.