Software and Computational Systems Lab

Publications of Philipp Wendler

1. Dirk Beyer, Nian-Ze Lee, and Philipp Wendler. Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification. Journal of Automated Reasoning, 2024. Keyword(s): CPAchecker, Software Model Checking PDF Supplement
   BibTeX Entry

   @article{IMC-JAR, author = {Dirk Beyer and Nian-Ze Lee and Philipp Wendler}, title = {Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification}, journal = {Journal of Automated Reasoning}, volume = {}, number = {}, pages = {}, year = {2024}, doi = {}, url = {https://www.sosy-lab.org/research/cpa-imc/}, pdf = {https://www.sosy-lab.org/research/pub/2024-JAR.Interpolation_and_SAT-Based_Model_Checking_Revisited_Adoption_to_Software_Verification.pdf}, keyword = {CPAchecker,Software Model Checking}, _sha256 = {}, }
2. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable Benchmarking: Requirements and Solutions. International Journal on Software Tools for Technology Transfer (STTT), 21(1):1-29, 2019. doi:10.1007/s10009-017-0469-y Keyword(s): Benchmarking Publisher's Version PDF Presentation Supplement
   Abstract

   Benchmarking is a widely used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in the International Competition on Software Verification, and is used by several research groups worldwide to ensure reliable benchmarking. Finally, we present guidelines on how to present measurement results in a scientifically valid and comprehensible way.
   BibTeX Entry

   @article{Benchmarking-STTT, author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler}, title = {Reliable Benchmarking: {R}equirements and Solutions}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {21}, number = {1}, pages = {1--29}, year = {2019}, doi = {10.1007/s10009-017-0469-y}, sha256 = {a50fbc212af394b32166d6354f986e7b1d5bc87220bdc50df899d6a46fedf33c}, url = {https://www.sosy-lab.org/research/benchmarking/}, presentation = {https://www.sosy-lab.org/research/prs/Latest_ReliableBenchmarking.pdf}, abstract = {Benchmarking is a widely used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in the International Competition on Software Verification, and is used by several research groups worldwide to ensure reliable benchmarking. Finally, we present guidelines on how to present measurement results in a scientifically valid and comprehensible way.}, keyword = {Benchmarking}, _pdf = {https://www.sosy-lab.org/research/pub/2019-STTT.Reliable_Benchmarking_Requirements_and_Solutions.pdf}, annote = {Publication appeared first online in November 2017<BR/> BenchExec is available at: <a href="https://github.com/sosy-lab/benchexec"> https://github.com/sosy-lab/benchexec</a>}, }
   Additional Infos

   Publication appeared first online in November 2017
   BenchExec is available at: https://github.com/sosy-lab/benchexec
3. Dirk Beyer, Matthias Dangl, and Philipp Wendler. A Unifying View on SMT-Based Software Verification. Journal of Automated Reasoning, 60(3):299-335, 2018. doi:10.1007/s10817-017-9432-6 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
   Abstract

   After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible presentation of four SMT-based verification approaches in order to study them in theory and in practice. We present and compare the following different "schools of thought" of software verification: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in the unifying theoretical framework of configurable program analysis and implement them in the verification framework CPAchecker. Based on this, we can present an evaluation that thoroughly compares the different approaches, where the core differences are expressed in configuration parameters and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches on a large set of verification tasks and discuss the conclusions.
   BibTeX Entry

   @article{AlgorithmComparison-JAR, author = {Dirk Beyer and Matthias Dangl and Philipp Wendler}, title = {A Unifying View on {SMT}-Based Software Verification}, journal = {Journal of Automated Reasoning}, volume = {60}, number = {3}, pages = {299--335}, year = {2018}, doi = {10.1007/s10817-017-9432-6}, sha256 = {5fab3eafacd7fef9c655afc9cd78bbb419ea47361a81633fb551fbf496875d84}, url = {https://www.sosy-lab.org/research/k-ind-compare/}, presentation = {https://www.sosy-lab.org/research/prs/Latest_UnifyingViewSmtBasedSoftwareVerification.pdf}, abstract = {After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible presentation of four SMT-based verification approaches in order to study them in theory and in practice. We present and compare the following different ``schools of thought'' of software verification: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in the unifying theoretical framework of configurable program analysis and implement them in the verification framework CPAchecker. Based on this, we can present an evaluation that thoroughly compares the different approaches, where the core differences are expressed in configuration parameters and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches on a large set of verification tasks and discuss the conclusions.}, keyword = {CPAchecker,Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2018-JAR.A_Unifying_View_on_SMT-Based_Software_Verification.pdf}, annote = {Publication appeared first online in December 2017<BR/> CPAchecker is available at: <a href="https://cpachecker.sosy-lab.org/"> https://cpachecker.sosy-lab.org/</a>}, issn = {1573-0670}, }
   Additional Infos

   Publication appeared first online in December 2017
   CPAchecker is available at: https://cpachecker.sosy-lab.org/
4. Philipp Wendler. Beiträge zu praktikabler Prädikatenanalyse. In S. Hölldobler, editors, Ausgezeichnete Informatikdissertationen 2017, LNI, pages 261-270, 2018. Gesellschaft für Informatik (GI). Keyword(s): Benchmarking, CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
   Abstract

   Der Stand der Forschung im Bereich der automatischen Software-Verifikation ist fragmentiert. Verschiedene Verfahren existieren nebeneinander in unterschiedlichen Darstellungen und mit wenig Bezug zueinander, aussagekräftige Vergleiche sind selten. Die Dissertation adressiert dieses Problem. Ein konfigurierbares und flexibles Rahmenwerk zur Vereinheitlichung solcher Verfahren wird entwickelt und mehrere vorhandene Verfahren werden in diesem Rahmenwerk ausgedrückt. Dies bringt neue Erkenntnisse über die Kernideen dieser Verfahren, ermöglicht experimentelle Studien in einer neuartigen Qualität, und erleichtert die Forschung an Kombinationen und Weiterentwicklungen dieser Verfahren. Die Implementierung dieses Rahmenwerks im erfolgreichen Verifizierer CPAchecker wird in der bisher größten derartigen experimentellen Studie (120 verschiedene Konfigurationen, 671280 Ausführungen) evaluiert. Hierzu wird ein Benchmarking-System präsentiert, das mit Hilfe moderner Technologien signifikante qualitative Messfehler existierender Systeme vermeidet.
   BibTeX Entry

   @incollection{DissZusammenfassungWendler, author = {Philipp Wendler}, title = {Beitr{\"{a}}ge zu praktikabler Pr{\"{a}}dikatenanalyse}, booktitle = {Ausgezeichnete Informatikdissertationen 2017}, editor = {S. H{\"{o}}lldobler}, volume = {{D-18}}, pages = {261-270}, year = {2018}, series = {{LNI}}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, isbn = {978-3885799771}, url = {https://www.sosy-lab.org/research/phd/wendler/}, pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/19476/invited_paper_4.pdf?sequence=1&isAllowed=y}, presentation = {https://www.sosy-lab.org/research/prs/2018-05-08_GiDiss_BeitraegeZuPraktikablerPraedikatenanalyse.pdf}, abstract = {Der Stand der Forschung im Bereich der automatischen Software-Verifikation ist fragmentiert. Verschiedene Verfahren existieren nebeneinander in unterschiedlichen Darstellungen und mit wenig Bezug zueinander, aussagekr&auml;ftige Vergleiche sind selten. Die Dissertation adressiert dieses Problem. Ein konfigurierbares und flexibles Rahmenwerk zur Vereinheitlichung solcher Verfahren wird entwickelt und mehrere vorhandene Verfahren werden in diesem Rahmenwerk ausgedr&uuml;ckt. Dies bringt neue Erkenntnisse &uuml;ber die Kernideen dieser Verfahren, erm&ouml;glicht experimentelle Studien in einer neuartigen Qualit&auml;t, und erleichtert die Forschung an Kombinationen und Weiterentwicklungen dieser Verfahren. Die Implementierung dieses Rahmenwerks im erfolgreichen Verifizierer CPAchecker wird in der bisher gr&ouml;&szlig;ten derartigen experimentellen Studie (120 verschiedene Konfigurationen, 671280 Ausf&uuml;hrungen) evaluiert. Hierzu wird ein Benchmarking-System pr&auml;sentiert, das mit Hilfe moderner Technologien signifikante qualitative Messfehler existierender Systeme vermeidet.}, keyword = {Benchmarking,CPAchecker,Software Model Checking}, annote = {This is a German summary of the dissertation <a href="https://www.sosy-lab.org/research/bib/Year/2017.complete.html#PhilippPredicateAnalysis">Towards Practical Predicate Analysis</a>.}, doifalse = {20.500.12116/19476}, urlpub = {https://dl.gi.de/handle/20.500.12116/19476}, }
   Additional Infos

   This is a German summary of the dissertation Towards Practical Predicate Analysis.

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

   1. doi:10.5281/zenodo.13612338
   Abstract

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

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

   An extended version of this article is available on arXiv.
6. Daniel Baier, Dirk Beyer, Po-Chun Chien, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch-Rosenfeld, Martin Spiessl, Henrik Wachowitz, and Philipp Wendler. CPAchecker 2.3 with Strategy Selection (Competition Contribution). In 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)

   1. doi:10.5281/zenodo.10203297
   Abstract

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

   @inproceedings{TACAS24c, author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Martin Spiessl and Henrik Wachowitz and Philipp Wendler}, title = {{CPAchecker} 2.3 with Strategy Selection (Competition Contribution)}, booktitle = {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}, }
7. Philipp Wendler and Stefan Winter. 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)

   1. doi:10.5281/zenodo.10639030
   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}, }
8. Dirk Beyer and Philipp Wendler. CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020, Dublin, Ireland, April 25-30), part 2, LNCS 12079, pages 126-133, 2020. Springer. doi:10.1007/978-3-030-45237-7_8 Keyword(s): Benchmarking Publisher's Version PDF Presentation Video Supplement
   Abstract

   Verification algorithms are among the most resource-intensive computation tasks. Saving energy is important for our living environment and to save cost in data centers. Yet, researchers compare the efficiency of algorithms still in terms of consumption of CPU time (or even wall time). Perhaps one reason for this is that measuring energy consumption of computational processes is not as convenient as measuring the consumed time and there is no sufficient tool support. To close this gap, we contribute CPU Energy Meter, a small tool that takes care of reading the energy values that Intel CPUs track inside the chip. In order to make energy measurements as easy as possible, we integrated CPU Energy Meter into BenchExec, a benchmarking tool that is already used by many researchers and competitions in the domain of formal methods. As evidence for usefulness, we explored the energy consumption of some state-of-the-art verifiers and report some interesting insights, for example, that energy consumption is not necessarily correlated with CPU time.
   BibTeX Entry

   @inproceedings{TACAS20b, author = {Dirk Beyer and Philipp Wendler}, title = {CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering}, booktitle = {Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2020, Dublin, Ireland, April 25-30), part 2}, pages = {126-133}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_8}, sha256 = {c5c8ad06f4b192e61799469a8fc6ca4661714aa2945e0ce07363a376ff06dcd7}, url = {https://www.sosy-lab.org/research/energy-measurement/}, presentation = {https://www.sosy-lab.org/research/prs/2021-03-31_TACAS20_CPU-Energy-Meter_Dirk.pdf}, abstract = {Verification algorithms are among the most resource-intensive computation tasks. Saving energy is important for our living environment and to save cost in data centers. Yet, researchers compare the efficiency of algorithms still in terms of consumption of CPU time (or even wall time). Perhaps one reason for this is that measuring energy consumption of computational processes is not as convenient as measuring the consumed time and there is no sufficient tool support. To close this gap, we contribute CPU Energy Meter, a small tool that takes care of reading the energy values that Intel CPUs track inside the chip. In order to make energy measurements as easy as possible, we integrated CPU Energy Meter into BenchExec, a benchmarking tool that is already used by many researchers and competitions in the domain of formal methods. As evidence for usefulness, we explored the energy consumption of some state-of-the-art verifiers and report some interesting insights, for example, that energy consumption is not necessarily correlated with CPU time.}, keyword = {Benchmarking}, video = {https://youtu.be/qzKAoBVTw2c}, }
9. Egor George Karpenkov, David Monniaux, and Philipp Wendler. Program Analysis with Local Policy Iteration. In Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016, St. Petersburg, FL, USA, January 17-19), LNCS 9583, pages 127-146, 2016. Springer-Verlag, Heidelberg. doi:10.1007/978-3-662-49122-5_6 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
   Abstract

   We present local policy iteration (LPI), a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis (CPA) framework, thus allowing inter-analysis communication. LPI uses adjustable-block encoding in order to traverse loop-free program sections, possibly containing branching, without introducing extra abstraction. Our technique operates over any template linear constraint domain, including the interval and octagon domains; templates can also be derived from the program source. The implementation is evaluated on a set of benchmarks from the International Competition on Software Verification (SV-COMP). It competes favorably with state-of-the-art analyzers.
   BibTeX Entry

   @inproceedings{LPI, author = {Egor George Karpenkov and David Monniaux and Philipp Wendler}, title = {Program Analysis with Local Policy Iteration}, booktitle = {Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI~2016, St.~Petersburg, FL, USA, January 17-19)}, pages = {127--146}, year = {2016}, series = {LNCS~9583}, publisher = {Springer-Verlag, Heidelberg}, doi = {10.1007/978-3-662-49122-5_6}, sha256 = {}, url = {http://lpi.metaworld.me}, pdf = {https://arxiv.org/pdf/1509.03424}, abstract = {We present local policy iteration (LPI), a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis (CPA) framework, thus allowing inter-analysis communication. LPI uses adjustable-block encoding in order to traverse loop-free program sections, possibly containing branching, without introducing extra abstraction. Our technique operates over any template linear constraint domain, including the interval and octagon domains; templates can also be derived from the program source. The implementation is evaluated on a set of benchmarks from the International Competition on Software Verification (SV-COMP). It competes favorably with state-of-the-art analyzers.}, keyword = {CPAchecker,Software Model Checking}, }
10. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Refinement Selection. In B. Fischer and J. Geldenhuys, editors, Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN 2015, Stellenbosch, South Africa, August 24-26), LNCS 9232, pages 20-38, 2015. Springer-Verlag, Heidelberg. doi:10.1007/978-3-319-23404-5_3 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    Counterexample-guided abstraction refinement is a property-directed approach for the automatic construction of an abstract model for a given system. The approach learns information from infeasible error paths in order to refine the abstract model. We address the problem of selecting which information to learn from a given infeasible error path. In previous work, we presented a method that enables refinement selection by extracting a set of sliced prefixes from a given infeasible error path, each of which represents a different reason for infeasibility of the error path and thus, a possible way to refine the abstract model. In this work, we (1) define and investigate several promising heuristics for selecting an appropriate precision for refinement, and (2) propose a new combination of a value analysis and a predicate analysis that does not only find out which information to learn from an infeasible error path, but automatically decides which analysis should be preferred for a refinement. These contributions allow a more systematic refinement strategy for CEGAR-based analyses. We evaluated the idea on software verification. We provide an implementation of the new concepts in the verification framework CPAchecker and make it publicly available. In a thorough experimental study, we show that refinement selection often avoids state-space explosion where existing approaches diverge, and that it can be even more powerful if applied on a higher level, where it decides which analysis of a combination should be favored for a refinement.
    BibTeX Entry

    @inproceedings{SPIN15b, author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler}, title = {Refinement Selection}, booktitle = {Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN~2015, Stellenbosch, South Africa, August 24-26)}, editor = {B.~Fischer and J.~Geldenhuys}, pages = {20-38}, year = {2015}, series = {LNCS~9232}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-319-23403-8}, doi = {10.1007/978-3-319-23404-5_3}, url = {https://www.sosy-lab.org/research/cpa-ref-sel/}, pdf = {https://www.sosy-lab.org/research/pub/2015-SPIN.Refinement_Selection.pdf}, abstract = {Counterexample-guided abstraction refinement is a property-directed approach for the automatic construction of an abstract model for a given system. The approach learns information from infeasible error paths in order to refine the abstract model. We address the problem of selecting which information to learn from a given infeasible error path. In previous work, we presented a method that enables refinement selection by extracting a set of sliced prefixes from a given infeasible error path, each of which represents a different reason for infeasibility of the error path and thus, a possible way to refine the abstract model. In this work, we (1) define and investigate several promising heuristics for selecting an appropriate precision for refinement, and (2) propose a new combination of a value analysis and a predicate analysis that does not only find out which information to learn from an infeasible error path, but automatically decides which analysis should be preferred for a refinement. These contributions allow a more systematic refinement strategy for CEGAR-based analyses. We evaluated the idea on software verification. We provide an implementation of the new concepts in the verification framework CPAchecker and make it publicly available. In a thorough experimental study, we show that refinement selection often avoids state-space explosion where existing approaches diverge, and that it can be even more powerful if applied on a higher level, where it decides which analysis of a combination should be favored for a refinement.}, keyword = {CPAchecker,Software Model Checking}, }
11. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Benchmarking and Resource Measurement. In B. Fischer and J. Geldenhuys, editors, Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN 2015, Stellenbosch, South Africa, August 24-26), LNCS 9232, pages 160-178, 2015. Springer-Verlag, Heidelberg. doi:10.1007/978-3-319-23404-5_12 Keyword(s): Benchmarking Publisher's Version PDF Supplement
    Abstract

    Proper benchmarking and resource measurement is an important topic, because benchmarking is a widely-used method for the comparative evaluation of tools and algorithms in many research areas. It is essential for researchers, tool developers, and users, as well as for competitions. We formulate a set of requirements that are indispensable for reproducible benchmarking and reliable resource measurement of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework is complex and can (on Linux) currently only be done by using the cgroups feature of the kernel. We provide BenchExec, a ready-to-use, tool-independent, and free implementation of a benchmarking framework that fulfills all presented requirements, making reproducible benchmarking and reliable resource measurement easy. Our framework is able to work with a wide range of different tools and has proven its reliability and usefulness in the International Competition on Software Verification.
    BibTeX Entry

    @inproceedings{SPIN15a, author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler}, title = {Benchmarking and Resource Measurement}, booktitle = {Proceedings of the 22nd International Symposium on Model Checking of Software (SPIN~2015, Stellenbosch, South Africa, August 24-26)}, editor = {B.~Fischer and J.~Geldenhuys}, pages = {160-178}, year = {2015}, series = {LNCS~9232}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-319-23403-8}, doi = {10.1007/978-3-319-23404-5_12}, url = {https://www.sosy-lab.org/research/benchmarking/}, pdf = {https://www.sosy-lab.org/research/pub/2015-SPIN.Benchmarking_and_Resource_Measurement.pdf}, abstract = {Proper benchmarking and resource measurement is an important topic, because benchmarking is a widely-used method for the comparative evaluation of tools and algorithms in many research areas. It is essential for researchers, tool developers, and users, as well as for competitions. We formulate a set of requirements that are indispensable for reproducible benchmarking and reliable resource measurement of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework is complex and can (on Linux) currently only be done by using the cgroups feature of the kernel. We provide BenchExec, a ready-to-use, tool-independent, and free implementation of a benchmarking framework that fulfills all presented requirements, making reproducible benchmarking and reliable resource measurement easy. Our framework is able to work with a wide range of different tools and has proven its reliability and usefulness in the International Competition on Software Verification.}, keyword = {Benchmarking}, annote = {An <a href="https://www.sosy-lab.org/research/bib/Year/2017.complete.html#Benchmarking-STTT">extended version</a> of this article appeared in STTT.}, }
    Additional Infos

    An extended version of this article appeared in STTT.
12. Dirk Beyer, Matthias Dangl, and Philipp Wendler. Boosting k-Induction with Continuously-Refined Invariants. In D. Kröning and C. S. Pasareanu, editors, Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015, San Francisco, CA, USA, July 18-24), LNCS 9206, pages 622-640, 2015. Springer-Verlag, Heidelberg. doi:10.1007/978-3-319-21690-4_42 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    k-Induction is a promising technique to extend bounded model checking from falsification to verification. In software verification, k-induction works only if auxiliary invariants are used to strengthen the induction hypothesis. The problem that we address is to generate such invariants (1) automatically without user-interaction, (2) efficiently such that little verification time is spent on the invariant generation, and (3) that are sufficiently strong for a k-induction proof. We boost the k-induction approach to significantly increase effectiveness and efficiency in the following way: We start in parallel to k-induction a data-flow-based invariant generator that supports dynamic precision adjustment and refine the precision of the invariant generator continuously during the analysis, such that the invariants become increasingly stronger. The k-induction engine is extended such that the invariants from the invariant generator are injected in each iteration to strengthen the hypothesis. The new method solves the above-mentioned problem because it (1) automatically chooses an invariant by step-wise refinement, (2) starts always with a lightweight invariant generation that is computationally inexpensive, and (3) refines the invariant precision more and more to inject stronger and stronger invariants into the induction system. We present and evaluate an implementation of our approach, as well as all other existing approaches, in the open-source verification-framework CPAchecker. Our experiments show that combining k-induction with continuously-refined invariants significantly increases effectiveness and efficiency, and outperforms all existing implementations of k-induction-based verification of C programs in terms of successful results.
    BibTeX Entry

    @inproceedings{CAV15, author = {Dirk Beyer and Matthias Dangl and Philipp Wendler}, title = {Boosting k-Induction with Continuously-Refined Invariants}, booktitle = {Proceedings of the 27th International Conference on Computer Aided Verification (CAV~2015, San Francisco, CA, USA, July 18-24)}, editor = {D.~Kr{\"o}ning and C.~S.~Pasareanu}, pages = {622-640}, year = {2015}, series = {LNCS~9206}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-319-21689-8}, doi = {10.1007/978-3-319-21690-4_42}, sha256 = {beb169351523c85e417e028c4e32b47c2c29e5db2e7b29ef8f5a2230e9562216}, url = {https://www.sosy-lab.org/research/cpa-k-induction/}, abstract = {k-Induction is a promising technique to extend bounded model checking from falsification to verification. In software verification, k-induction works only if auxiliary invariants are used to strengthen the induction hypothesis. The problem that we address is to generate such invariants (1) automatically without user-interaction, (2) efficiently such that little verification time is spent on the invariant generation, and (3) that are sufficiently strong for a k-induction proof. We boost the k-induction approach to significantly increase effectiveness and efficiency in the following way: We start in parallel to k-induction a data-flow-based invariant generator that supports dynamic precision adjustment and refine the precision of the invariant generator continuously during the analysis, such that the invariants become increasingly stronger. The k-induction engine is extended such that the invariants from the invariant generator are injected in each iteration to strengthen the hypothesis. The new method solves the above-mentioned problem because it (1) automatically chooses an invariant by step-wise refinement, (2) starts always with a lightweight invariant generation that is computationally inexpensive, and (3) refines the invariant precision more and more to inject stronger and stronger invariants into the induction system. We present and evaluate an implementation of our approach, as well as all other existing approaches, in the open-source verification-framework CPAchecker. Our experiments show that combining k-induction with continuously-refined invariants significantly increases effectiveness and efficiency, and outperforms all existing implementations of k-induction-based verification of C programs in terms of successful results.}, keyword = {CPAchecker,Software Model Checking}, }
13. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Sliced Path Prefixes: An Effective Method to Enable Refinement Selection. In S. Graf and M. Viswanathan, editors, Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015, Grenoble, France, June 2-4), LNCS 9039, pages 228-243, 2015. Springer-Verlag, Heidelberg. doi:10.1007/978-3-319-19195-9_15 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    Automatic software verification relies on constructing, for a given program, an abstract model that is (1) abstract enough to avoid state-space explosion and (2) precise enough to reason about the specification. Counterexample-guided abstraction refinement is a standard technique that suggests to extract information from infeasible error paths, in order to refine the abstract model if it is too imprecise. Existing approaches -including our previous work- do not choose the refinement for a given path systematically. We present a method that generates alternative refinements and allows to systematically choose a suited one. The method takes as input one given infeasible error path and applies a slicing technique to obtain a set of new error paths that are more abstract than the original error path but still infeasible, each for a different reason. The (more abstract) constraints of the new paths can be passed to a standard refinement procedure, in order to obtain a set of possible refinements, one for each new path. Our technique is completely independent from the abstract domain that is used in the program analysis, and does not rely on a certain proof technique, such as SMT solving. We implemented the new algorithm in the verification framework CPAchecker and made our extension publicly available. The experimental evaluation of our technique indicates that there is a wide range of possibilities on how to refine the abstract model for a given error path, and we demonstrate that the choice of which refinement to apply to the abstract model has a significant impact on the verification effectiveness and efficiency.
    BibTeX Entry

    @inproceedings{FORTE15, author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler}, title = {Sliced Path Prefixes: An Effective Method to Enable Refinement Selection}, booktitle = {Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE~2015, Grenoble, France, June 2-4)}, editor = {S.~Graf and M.~Viswanathan}, pages = {228-243}, year = {2015}, series = {LNCS~9039}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-319-19194-2}, doi = {10.1007/978-3-319-19195-9_15}, sha256 = {96e16841eb13a602455334a71a516f509ad1b1e2328edade3d5954062b387e7d}, url = {https://www.sosy-lab.org/research/cpa-ref-sel/#FORTE15}, abstract = {Automatic software verification relies on constructing, for a given program, an abstract model that is (1) abstract enough to avoid state-space explosion and (2) precise enough to reason about the specification. Counterexample-guided abstraction refinement is a standard technique that suggests to extract information from infeasible error paths, in order to refine the abstract model if it is too imprecise. Existing approaches ---including our previous work--- do not choose the refinement for a given path systematically. We present a method that generates alternative refinements and allows to systematically choose a suited one. The method takes as input one given infeasible error path and applies a slicing technique to obtain a set of new error paths that are more abstract than the original error path but still infeasible, each for a different reason. The (more abstract) constraints of the new paths can be passed to a standard refinement procedure, in order to obtain a set of possible refinements, one for each new path. Our technique is completely independent from the abstract domain that is used in the program analysis, and does not rely on a certain proof technique, such as SMT solving. We implemented the new algorithm in the verification framework CPAchecker and made our extension publicly available. The experimental evaluation of our technique indicates that there is a wide range of possibilities on how to refine the abstract model for a given error path, and we demonstrate that the choice of which refinement to apply to the abstract model has a significant impact on the verification effectiveness and efficiency.}, keyword = {CPAchecker,Software Model Checking}, }
14. Matthias Dangl, Stefan Löwe, and Philipp Wendler. CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic (Competition Contribution). In C. Baier and C. Tinelli, editors, Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015, London, UK, April 13-17), LNCS 9035, pages 423-425, 2015. Springer-Verlag, Heidelberg. doi:10.1007/978-3-662-46681-0_34 Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
    Abstract

    We submit to SV-COMP'15 the software-verification framework CPAchecker. The submitted configuration is a combination of seven different analyses, based on explicit-value analysis, k-induction, predicate analysis, and concrete memory graphs. These analyses use concepts such as CEGAR, lazy abstraction, interpolation, adjustable-block encoding, bounded model checking, invariant generation, and block-abstraction memoization. Found counterexamples are cross-checked by a bit-precise analysis. The combination of several different analyses copes well with the diversity of the verification tasks in SV-COMP.
    BibTeX Entry

    @inproceedings{CPACHECKER-COMP15, author = {Matthias Dangl and Stefan L{\"{o}}we and Philipp Wendler}, title = {{{\sc CPAchecker}} with Support for Recursive Programs and Floating-Point Arithmetic (Competition Contribution)}, booktitle = {Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2015, London, UK, April 13-17)}, editor = {C.~Baier and C.~Tinelli}, pages = {423--425}, year = {2015}, series = {LNCS~9035}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-662-46680-3}, doi = {10.1007/978-3-662-46681-0_34}, sha256 = {}, url = {https://doi.org/10.1007/978-3-662-46681-0_34}, pdf = {https://www.sosy-lab.org/research/pub/2015-TACAS.CPAchecker_with_Support_for_Recursive_Programs_and_Floating-Point_Arithmetic.pdf}, abstract = {We submit to SV-COMP'15 the software-verification framework CPAchecker. The submitted configuration is a combination of seven different analyses, based on explicit-value analysis, k-induction, predicate analysis, and concrete memory graphs. These analyses use concepts such as CEGAR, lazy abstraction, interpolation, adjustable-block encoding, bounded model checking, invariant generation, and block-abstraction memoization. Found counterexamples are cross-checked by a bit-precise analysis. The combination of several different analyses copes well with the diversity of the verification tasks in SV-COMP.}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, annote = {Won categories ControlFlow, MemorySafety, and Overall, and received three silver and two bronze medals in <span style="white-space: nowrap"><a href="https://sv-comp.sosy-lab.org/2015/">SV-COMP'15</a></span>}, }
    Additional Infos

    Won categories ControlFlow, MemorySafety, and Overall, and received three silver and two bronze medals in SV-COMP'15
15. Dirk Beyer, Georg Dresler, and Philipp Wendler. Software Verification in the Google App-Engine Cloud. In A. Biere and R. Bloem, editors, Proceedings of the 26th International Conference on Computer-Aided Verification (CAV 2014, Vienna, Austria, July 18-22), LNCS 8559, pages 327-333, 2014. Springer-Verlag, Heidelberg. doi:10.1007/978-3-319-08867-9_21 Keyword(s): CPAchecker, Software Model Checking, Cloud-Based Software Verification Publisher's Version PDF Supplement
    Abstract

    Software verification often requires a large amount of computing resources. In the last years, cloud services emerged as an inexpensive, flexible, and energy-efficient source of computing power. We have investigated if such cloud resources can be used effectively for verification. We chose the platform-as-a-service offer Google App Engine and ported the open-source verification framework CPAchecker to it. We provide our new verification service as a web front-end to users who wish to solve single verification tasks (tutorial usage), and an API for integrating the service into existing verification infrastructures (massively parallel bulk usage). We experimentally evaluate the effectiveness of this service and show that it can be successfully used to offload verification work to the cloud, considerably sparing local verification resources.
    BibTeX Entry

    @inproceedings{CAV14, author = {Dirk Beyer and Georg Dresler and Philipp Wendler}, title = {Software Verification in the {Google} {App-Engine} Cloud}, booktitle = {Proceedings of the 26th International Conference on Computer-Aided Verification (CAV~2014, Vienna, Austria, July 18-22)}, editor = {A.~Biere and R.~Bloem}, pages = {327-333}, year = {2014}, series = {LNCS~8559}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-319-08866-2}, doi = {10.1007/978-3-319-08867-9_21}, sha256 = {f92060721e703c8553d5420c34f07eea24fe25d36ae9c02217688606e1898704}, url = {http://www.sosy-lab.org/~dbeyer/cpa-appengine}, abstract = {Software verification often requires a large amount of computing resources. In the last years, cloud services emerged as an inexpensive, flexible, and energy-efficient source of computing power. We have investigated if such cloud resources can be used effectively for verification. We chose the platform-as-a-service offer Google App Engine and ported the open-source verification framework CPAchecker to it. We provide our new verification service as a web front-end to users who wish to solve single verification tasks (tutorial usage), and an API for integrating the service into existing verification infrastructures (massively parallel bulk usage). We experimentally evaluate the effectiveness of this service and show that it can be successfully used to offload verification work to the cloud, considerably sparing local verification resources.}, keyword = {CPAchecker,Software Model Checking,Cloud-Based Software Verification}, }
16. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Precision Reuse in CPAchecker. In W. Hasselbring and N. C. Ehmke, editors, Tagungsband Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik (25. Februar - 28. Februar 2014, Kiel, Deutschland), LNI 227, pages 41-42, 2014. Gesellschaft für Informatik (GI). Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
    Abstract

    Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.
    BibTeX Entry

    @inproceedings{SE14-Reuse, author = {Dirk Beyer and Stefan L{\"{o}}we and Evgeny Novikov and Andreas Stahlbauer and Philipp Wendler}, title = {Precision Reuse in CPAchecker}, booktitle = {Tagungsband Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik (25. Februar - 28. Februar 2014, Kiel, Deutschland)}, editor = {W.~Hasselbring and N.~C.~Ehmke}, pages = {41--42}, year = {2014}, series = {{LNI}~227}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, pdf = {https://dl.gi.de/bitstream/handle/20.500.12116/30949/041.pdf?sequence=1&isAllowed=y}, abstract = {Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.}, keyword = {CPAchecker,Software Model Checking}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2013.html#FSE13">full article on this topic</a> that appeared in Proc. ESEC/FSE 2013.}, doinone = {DOI not available}, urlpub = {https://dl.gi.de/handle/20.500.12116/30949}, }
    Additional Infos

    This is a summary of a full article on this topic that appeared in Proc. ESEC/FSE 2013.
17. Stefan Löwe, Mikhail U. Mandrykin, and Philipp Wendler. CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution). In E. Abraham and K. Havelund, editors, Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014, Grenoble, France, April 5-13), LNCS 8413, pages 392-394, 2014. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-54862-8_27 Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
    Abstract

    CPAchecker is a framework for software verification, built on the foundations of configurable program analysis (CPA). For the SV-COMP'14, we file a CPAchecker configuration that runs up to five analyses in sequence. The first two analyses of our approach utilize the explicit-value domain for modeling the state space, while the remaining analyses are based on predicate abstraction. In addition to that, a bit-precise counterexample checker comes into action whenever an analysis finds a counterexample. The combination of conceptually different analyses is key to the success of our verification approach, as the diversity of verification tasks is taken into account.
    BibTeX Entry

    @inproceedings{CPACHECKER-COMP14, author = {Stefan~L{\"{o}}we and Mikhail~U.~Mandrykin and Philipp~Wendler}, title = {{{\sc CPAchecker}} with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution)}, booktitle = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2014, Grenoble, France, April 5-13)}, editor = {E.~Abraham and K. Havelund}, pages = {392-394}, year = {2014}, series = {LNCS~8413}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-642-54861-1}, doi = {10.1007/978-3-642-54862-8_27}, sha256 = {}, url = {https://doi.org/10.1007/978-3-642-54862-8_27}, pdf = {https://www.sosy-lab.org/research/pub/2014-TACAS.CPAchecker_with_Sequential_Combination_of_Explicit-Value_Analyses_and_Predicate_Analyses.pdf}, abstract = {CPAchecker is a framework for software verification, built on the foundations of configurable program analysis (CPA). For the SV-COMP'14, we file a CPAchecker configuration that runs up to five analyses in sequence. The first two analyses of our approach utilize the explicit-value domain for modeling the state space, while the remaining analyses are based on predicate abstraction. In addition to that, a bit-precise counterexample checker comes into action whenever an analysis finds a counterexample. The combination of conceptually different analyses is key to the success of our verification approach, as the diversity of verification tasks is taken into account.}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, annote = {Won categories ControlFlow, MemorySafety, and Simple, and received one silver and one bronze medal in <span style="white-space: nowrap"><a href="https://sv-comp.sosy-lab.org/2014/">SV-COMP'14</a></span>}, }
    Additional Infos

    Won categories ControlFlow, MemorySafety, and Simple, and received one silver and one bronze medal in SV-COMP'14
18. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Precision Reuse for Efficient Regression Verification. In B. Meyer, L. Baresi, and M. Mezini, editors, Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2013, St. Petersburg, Russia, August 18-26), pages 389-399, 2013. ACM. doi:10.1145/2491411.2491429 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.
    BibTeX Entry

    @inproceedings{FSE13, author = {Dirk Beyer and Stefan L{\"o}we and Evgeny Novikov and Andreas Stahlbauer and Philipp Wendler}, title = {Precision Reuse for Efficient Regression Verification}, booktitle = {Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2013, St. Petersburg, Russia, August 18-26)}, editor = {B.~Meyer and L.~Baresi and M.~Mezini}, pages = {389-399}, year = {2013}, publisher = {ACM}, isbn = {}, doi = {10.1145/2491411.2491429}, url = {https://www.sosy-lab.org/research/cpa-reuse/}, pdf = {https://www.sosy-lab.org/research/pub/2013-FSE.Precision_Reuse_for_Efficient_Regression_Verification.pdf}, abstract = {Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.}, keyword = {CPAchecker,Software Model Checking}, }
19. Dirk Beyer and Philipp Wendler. Reuse of Verification Results: Conditional Model Checking, Precision Reuse, and Verification Witnesses. In E. Bartocci and C. R. Ramakrishnan, editors, Proceedings of the 2013 International Symposium on Model Checking of Software (SPIN 2013, Stony Brook, NY, USA, July 8-9), LNCS 7976, pages 1-17, 2013. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-39176-7_1 Keyword(s): Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Publisher's Version PDF Supplement
    Abstract

    Verification is a complex algorithmic task, requiring large amounts of computing resources. One approach to reduce the resource consumption is to reuse information from previous verification runs. This paper gives an overview of three techniques for such information reuse. Conditional model checking outputs a condition that describes the state space that was successfully verified, and accepts as input a condition that instructs the model checker which parts of the system should be verified; thus, later verification runs can use the output condition of previous runs in order to not verify again parts of the state space that were already verified. Precision reuse is a technique to use intermediate results from previous verification runs to accelerate further verification runs of the system; information about the level of abstraction in the abstract model can be reused in later verification runs. Typical model checkers provide an error path through the system as witness for having proved that a system violates a property, and a few model checkers provide some kind of proof certificate as a witness for the correctness of the system; these witnesses should be such that the verifiers can read them and -with less computational effort- (re-) verify that the witness is valid.
    BibTeX Entry

    @inproceedings{SPIN13, author = {Dirk Beyer and Philipp Wendler}, title = {Reuse of Verification Results: Conditional Model Checking, Precision Reuse, and Verification Witnesses}, booktitle = {Proceedings of the 2013 International Symposium on Model Checking of Software (SPIN~2013, Stony Brook, NY, USA, July 8-9)}, editor = {E.~Bartocci and C.~R.~Ramakrishnan}, pages = {1-17}, year = {2013}, series = {LNCS~7976}, publisher = {Springer-Verlag, Heidelberg}, isbn = {}, doi = {10.1007/978-3-642-39176-7_1}, sha256 = {}, url = {http://www.sosy-lab.org/~dbeyer/cpa-reuse-gen/}, pdf = {https://www.sosy-lab.org/research/pub/2013-SPIN.Reuse_of_Verification_Results.pdf}, abstract = {Verification is a complex algorithmic task, requiring large amounts of computing resources. One approach to reduce the resource consumption is to reuse information from previous verification runs. This paper gives an overview of three techniques for such information reuse. Conditional model checking outputs a condition that describes the state space that was successfully verified, and accepts as input a condition that instructs the model checker which parts of the system should be verified; thus, later verification runs can use the output condition of previous runs in order to not verify again parts of the state space that were already verified. Precision reuse is a technique to use intermediate results from previous verification runs to accelerate further verification runs of the system; information about the level of abstraction in the abstract model can be reused in later verification runs. Typical model checkers provide an error path through the system as witness for having proved that a system violates a property, and a few model checkers provide some kind of proof certificate as a witness for the correctness of the system; these witnesses should be such that the verifiers can read them and ---with less computational effort--- (re-) verify that the witness is valid.}, keyword = {Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
20. Sven Apel, Alexander von Rhein, Philipp Wendler, Armin Größlinger, and Dirk Beyer. Strategies for Product-Line Verification: Case Studies and Experiments. In D. Notkin, B. H. C. Cheng, and K. Pohl, editors, Proceedings of the 35th International Conference on Software Engineering (ICSE 2013, San Francisco, CA, USA, May 18-26), pages 482-491, 2013. IEEE. doi:10.1109/ICSE.2013.6606594 Keyword(s): Software Model Checking Publisher's Version PDF Supplement
    Abstract

    Product-line technology is increasingly used in mission-critical and safety-critical applications. Hence, researchers are developing verification approaches that follow different strategies to cope with the specific properties of product lines. While the research community is discussing the mutual strengths and weaknesses of the different strategies-mostly at a conceptual level-there is a lack of evidence in terms of case studies, tool implementations, and experiments. We have collected and prepared six product lines as subject systems for experimentation. Furthermore, we have developed a model-checking tool chain for C-based and Java-based product lines, called SPLverifier, which we use to compare sample-based and family-based strategies with regard to verification performance and the ability to find defects. Based on the experimental results and an analytical model, we revisit the discussion of the strengths and weaknesses of product-line-verification strategies.
    BibTeX Entry

    @inproceedings{ICSE13, author = {Sven Apel and Alexander von Rhein and Philipp Wendler and Armin Gr{\"o}{\ss}linger and Dirk Beyer}, title = {Strategies for Product-Line Verification: Case Studies and Experiments}, booktitle = {Proceedings of the 35th International Conference on Software Engineering (ICSE~2013, San Francisco, CA, USA, May 18-26)}, editor = {D.~Notkin and B.~H.~C.~Cheng and K.~Pohl}, pages = {482-491}, year = {2013}, publisher = {IEEE}, isbn = {978-1-4673-3076-3}, doi = {10.1109/ICSE.2013.6606594}, url = {http://fosd.net/FAV}, pdf = {https://www.sosy-lab.org/research/pub/2013-ICSE.Strategies_for_Product-Line_Verification.pdf}, abstract = {Product-line technology is increasingly used in mission-critical and safety-critical applications. Hence, researchers are developing verification approaches that follow different strategies to cope with the specific properties of product lines. While the research community is discussing the mutual strengths and weaknesses of the different strategies---mostly at a conceptual level---there is a lack of evidence in terms of case studies, tool implementations, and experiments. We have collected and prepared six product lines as subject systems for experimentation. Furthermore, we have developed a model-checking tool chain for C-based and Java-based product lines, called SPLverifier, which we use to compare sample-based and family-based strategies with regard to verification performance and the ability to find defects. Based on the experimental results and an analytical model, we revisit the discussion of the strengths and weaknesses of product-line--verification strategies.}, keyword = {Software Model Checking}, }
21. Philipp Wendler. CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution). In N. Piterman and S. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013, Rome, Italy, March 16-24), LNCS 7795, pages 613-615, 2013. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-36742-7_45 Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
    Abstract

    CPAchecker is an open-source framework for software verification, based on the concepts of configurable program analysis (CPA). We submit a CPAchecker configuration that uses a sequential combination of two approaches. It starts with an explicit-state analysis, and, if no answer can be found within some time, switches to a predicate analysis with adjustable-block encoding and CEGAR.
    BibTeX Entry

    @inproceedings{CPACHECKERSEQCOM-COMP13, author = {Philipp Wendler}, title = {{{\sc CPAchecker}} with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution)}, booktitle = {Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2013, Rome, Italy, March 16-24)}, editor = {N.~Piterman and S.~Smolka}, pages = {613-615}, year = {2013}, series = {LNCS~7795}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-642-36741-0}, doi = {10.1007/978-3-642-36742-7_45}, sha256 = {}, url = {https://doi.org/10.1007/978-3-642-36742-7_45}, pdf = {https://www.sosy-lab.org/research/pub/2013-TACAS.CPAchecker_with_Sequential_Combination_of_Explicit-State_Analysis_and_Predicate_Analysis.pdf}, abstract = {CPAchecker is an open-source framework for software verification, based on the concepts of configurable program analysis (CPA). We submit a CPAchecker configuration that uses a sequential combination of two approaches. It starts with an explicit-state analysis, and, if no answer can be found within some time, switches to a predicate analysis with adjustable-block encoding and CEGAR.}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, annote = {Won category Overall and received five bronze medals in <span style="white-space: nowrap"><a href="https://sv-comp.sosy-lab.org/2013/">SV-COMP'13</a></span>}, }
    Additional Infos

    Won category Overall and received five bronze medals in SV-COMP'13
22. Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, and Philipp Wendler. Conditional Model Checking: A Technique to Pass Information between Verifiers. In Tevfik Bultan and Martin Robillard, editors, Proceedings of the 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2012, Cary, NC, November 10-17), 2012. ACM. doi:10.1145/2393596.2393664 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P -usually a state predicate- such that the program satisfies the specification under the condition P -that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.
    BibTeX Entry

    @inproceedings{FSE12, author = {Dirk Beyer and Thomas A. Henzinger and M. Erkan Keremoglu and Philipp Wendler}, title = {Conditional Model Checking: {A} Technique to Pass Information between Verifiers}, booktitle = {Proceedings of the 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE~2012, Cary, NC, November 10-17)}, editor = {Tevfik Bultan and Martin Robillard}, pages = {}, year = {2012}, publisher = {ACM}, isbn = {978-1-4503-1614-9}, doi = {10.1145/2393596.2393664}, url = {https://www.sosy-lab.org/research/cpa-cmc/}, pdf = {https://www.sosy-lab.org/research/pub/2012-FSE.Conditional_Model_Checking.pdf}, abstract = {Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.}, keyword = {CPAchecker,Software Model Checking}, }
23. Dirk Beyer and Philipp Wendler. Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT. In Gianpiero Cabodi and Satnam Singh, editors, Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2012, Cambrige, UK, October 22-25), pages 106-113, 2012. FMCAD. Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    CEGAR, SMT solving, and Craig interpolation are successful approaches for software model checking. We compare two of the most important algorithms that are based on these techniques: lazy predicate abstraction (as in BLAST) and lazy abstraction with interpolants (as in IMPACT). We unify the algorithms formally (by expressing both in the CPA framework) as well as in practice (by implementing them in the same tool). This allows us to flexibly experiment with new configurations and gain new insights, both about their most important differences and commonalities, as well as about their performance characteristics. We show that the essential contribution of the IMPACT algorithm is the reduction of the number of refinements, and compare this to another approach for reducing refinement effort: adjustable-block encoding (ABE).
    BibTeX Entry

    @inproceedings{FMCAD12, author = {Dirk Beyer and Philipp Wendler}, title = {Algorithms for Software Model Checking: Predicate Abstraction vs. {IMPACT}}, booktitle = {Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD~2012, Cambrige, UK, October 22-25)}, editor = {Gianpiero Cabodi and Satnam Singh}, pages = {106-113}, year = {2012}, publisher = {FMCAD}, isbn = {978-1-4673-4831-7}, url = {https://www.sosy-lab.org/research/cpa-uni/}, pdf = {https://www.sosy-lab.org/research/pub/2012-FMCAD.Algorithms_for_Software_Model_Checking.pdf}, abstract = {CEGAR, SMT solving, and Craig interpolation are successful approaches for software model checking. We compare two of the most important algorithms that are based on these techniques: lazy predicate abstraction (as in BLAST) and lazy abstraction with interpolants (as in IMPACT). We unify the algorithms formally (by expressing both in the CPA framework) as well as in practice (by implementing them in the same tool). This allows us to flexibly experiment with new configurations and gain new insights, both about their most important differences and commonalities, as well as about their performance characteristics. We show that the essential contribution of the IMPACT algorithm is the reduction of the number of refinements, and compare this to another approach for reducing refinement effort: adjustable-block encoding (ABE).}, keyword = {CPAchecker,Software Model Checking}, doinone = {DOI not available}, urlpub = {https://ieeexplore.ieee.org/document/6462562/}, }
24. Stefan Löwe and Philipp Wendler. CPAchecker with Adjustable Predicate Analysis (Competition Contribution). In C. Flanagan and B. König, editors, Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012, Tallinn, Estonia, March 27-30), LNCS 7214, pages 528-530, 2012. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-28756-5_40 Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
    Abstract

    CPAchecker is a freely available software-verification framework, built on the concepts of configurable program analysis (CPA). CPAchecker integrates most of the state-of-the-art technologies for software model checking, such as counterexample-guided abstraction refinement (CEGAR), lazy predicate abstraction, interpolation-based refinement, and large-block encoding. The CPA for predicate analysis with adjustable-block encoding (ABE) is very promising in many categories, and thus, we submit a CPAchecker configuration that uses this analysis approach to the competition.
    BibTeX Entry

    @inproceedings{CPACHECKERABE-COMP12, author = {Stefan L{\"{o}}we and Philipp Wendler}, title = {{{\sc CPAchecker}} with Adjustable Predicate Analysis (Competition Contribution)}, booktitle = {Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2012, Tallinn, Estonia, March 27-30)}, editor = {C.~Flanagan and B.~K{\"o}nig}, pages = {528--530}, year = {2012}, series = {LNCS~7214}, publisher = {Springer-Verlag, Heidelberg}, doi = {10.1007/978-3-642-28756-5_40}, sha256 = {}, url = {https://doi.org/10.1007/978-3-642-28756-5_40}, pdf = {https://www.sosy-lab.org/research/pub/2012-TACAS.CPAchecker_with_Adjustable_Predicate_Analysis.pdf}, abstract = {CPAchecker is a freely available software-verification framework, built on the concepts of configurable program analysis (CPA). CPAchecker integrates most of the state-of-the-art technologies for software model checking, such as counterexample-guided abstraction refinement (CEGAR), lazy predicate abstraction, interpolation-based refinement, and large-block encoding. The CPA for predicate analysis with adjustable-block encoding (ABE) is very promising in many categories, and thus, we submit a CPAchecker configuration that uses this analysis approach to the competition.}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, annote = {Won category ControlFlowInteger and received one silver and two bronze medals in <span style="white-space: nowrap"><a href="https://sv-comp.sosy-lab.org/2012/">SV-COMP'12</a></span>}, }
    Additional Infos

    Won category ControlFlowInteger and received one silver and two bronze medals in SV-COMP'12
25. Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. Detection of Feature Interactions using Feature-Aware Verification. In Proceedings of the 26th International Conference on Automated Software Engineering (ASE 2011, Lawrence, KS, November 6-10), pages 372-375, 2011. IEEE. doi:10.1109/ASE.2011.6100075 Keyword(s): Software Model Checking Publisher's Version PDF Supplement
    Abstract

    A software product line is a set of software products that are distinguished in terms of features (i.e., end-user-visible units of behavior). Feature interactions -situations in which the combination of features leads to emergent and possibly critical behavior- are a major source of failures in software product lines. We explore how feature-aware verification can improve the automatic detection of feature interactions in software product lines. Feature-aware verification uses product-line-verification techniques and supports the specification of feature properties along with the features in separate and composable units. It integrates the technique of variability encoding to verify a product line without generating and checking a possibly exponential number of feature combinations. We developed the tool suite SPLverifier for feature-aware verification, which is based on standard model-checking technology. We applied it to an e-mail system that incorporates domain knowledge of AT&T. We found that feature interactions can be detected automatically based on specifications that have only local knowledge.
    BibTeX Entry

    @inproceedings{ASE11, author = {Sven Apel and Hendrik Speidel and Philipp Wendler and Alexander von Rhein and Dirk Beyer}, title = {Detection of Feature Interactions using Feature-Aware Verification}, booktitle = {Proceedings of the 26th International Conference on Automated Software Engineering (ASE~2011, Lawrence, KS, November 6-10)}, pages = {372-375}, year = {2011}, publisher = {IEEE}, isbn = {978-1-4577-1639-3}, doi = {10.1109/ASE.2011.6100075}, url = {http://fosd.net/FAV}, pdf = {https://www.sosy-lab.org/research/pub/2011-ASE.Detection_of_Feature_Interactions_using_Feature-Aware_Verification.pdf}, abstract = {A software product line is a set of software products that are distinguished in terms of features (i.e., end-user--visible units of behavior). Feature interactions ---situations in which the combination of features leads to emergent and possibly critical behavior--- are a major source of failures in software product lines. We explore how feature-aware verification can improve the automatic detection of feature interactions in software product lines. Feature-aware verification uses product-line--verification techniques and supports the specification of feature properties along with the features in separate and composable units. It integrates the technique of variability encoding to verify a product line without generating and checking a possibly exponential number of feature combinations. We developed the tool suite SPLverifier for feature-aware verification, which is based on standard model-checking technology. We applied it to an e-mail system that incorporates domain knowledge of AT&T. We found that feature interactions can be detected automatically based on specifications that have only local knowledge.}, keyword = {Software Model Checking}, }
26. Dirk Beyer, M. Erkan Keremoglu, and Philipp Wendler. Predicate Abstraction with Adjustable-Block Encoding. In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010, Lugano, October 20-23), pages 189-197, 2010. FMCAD. Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    Several successful software model checkers are based on a technique called single-block encoding (SBE), which computes costly predicate abstractions after every single program operation. Large-block encoding (LBE) computes abstractions only after a large number of operations, and it was shown that this significantly improves the verification performance. In this work, we present adjustable-block encoding (ABE), a unifying framework that allows to express both previous approaches. In addition, it provides the flexibility to specify any block size between SBE and LBE, and also beyond LBE, through the adjustment of one single parameter. Such a unification of different concepts makes it easier to understand the fundamental properties of the analysis, and makes the differences of the variants more explicit. We evaluate different configurations on example C programs, and identify one that is currently the best.
    BibTeX Entry

    @inproceedings{FMCAD10, author = {Dirk Beyer and M.~Erkan Keremoglu and Philipp Wendler}, title = {Predicate Abstraction with Adjustable-Block Encoding}, booktitle = {Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD~2010, Lugano, October 20-23)}, pages = {189-197}, year = {2010}, publisher = {FMCAD}, isbn = {}, url = {http://www.sosy-lab.org/~dbeyer/cpa-abe/}, pdf = {https://www.sosy-lab.org/research/pub/2010-FMCAD.Predicate_Abstraction_with_Adjustable-Block_Encoding.pdf}, abstract = {Several successful software model checkers are based on a technique called single-block encoding (SBE), which computes costly predicate abstractions after every single program operation. Large-block encoding (LBE) computes abstractions only after a large number of operations, and it was shown that this significantly improves the verification performance. In this work, we present adjustable-block encoding (ABE), a unifying framework that allows to express both previous approaches. In addition, it provides the flexibility to specify any block size between SBE and LBE, and also beyond LBE, through the adjustment of one single parameter. Such a unification of different concepts makes it easier to understand the fundamental properties of the analysis, and makes the differences of the variants more explicit. We evaluate different configurations on example C programs, and identify one that is currently the best.}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems}, doinone = {DOI not available}, urlpub = {https://ieeexplore.ieee.org/document/5770949/}, }
    Additional Infos

    Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems

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

    1. doi:10.5281/zenodo.13612338
    Abstract

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

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

    This technical report is an extended version of our paper at FM 2024.
28. Dirk Beyer, Nian-Ze Lee, and Philipp Wendler. Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification. Technical report 2208.05046, arXiv/CoRR, August 2022. doi:10.48550/arXiv.2208.05046 Keyword(s): Software Model Checking, CPAchecker Publisher's Version PDF Presentation Supplement
    Abstract

    Interpolation-based model checking (McMillan, 2003) is a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. The algorithm is state-of-the-art in hardware model checking. It derives interpolants from unsatisfiable BMC queries, and collects them to construct an overapproximation of the set of reachable states. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's interpolation-based model checking algorithm from 2003 has not been used to verify programs so far. This paper closes this significant, 19 years old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker, and evaluated the implementation against other state-of-the-art software-verification techniques over the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that interpolation-based model checking is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results might have important implications for software verification, because researchers and developers now have a richer set of approaches to choose from.
    BibTeX Entry

    @techreport{TechReport22a, author = {Dirk Beyer and Nian-Ze Lee and Philipp Wendler}, title = {Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification}, number = {2208.05046}, year = {2022}, doi = {10.48550/arXiv.2208.05046}, url = {https://www.sosy-lab.org/research/cpa-imc/}, presentation = {https://www.sosy-lab.org/research/prs/2022-08-11_iPRA22_Interpolation_and_SAT-Based_Model_Checking_Revisited.pdf}, abstract = {Interpolation-based model checking <a href="https://doi.org/10.1007/978-3-540-45069-6_1">(McMillan, 2003)</a> is a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. The algorithm is state-of-the-art in hardware model checking. It derives interpolants from unsatisfiable BMC queries, and collects them to construct an overapproximation of the set of reachable states. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's <em>interpolation-based model checking</em> algorithm from 2003 has not been used to verify programs so far. This paper closes this significant, 19 years old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker, and evaluated the implementation against other state-of-the-art software-verification techniques over the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that interpolation-based model checking is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results might have important implications for software verification, because researchers and developers now have a richer set of approaches to choose from.}, keyword = {Software Model Checking, CPAchecker}, _pdf = {https://www.sosy-lab.org/research/cpa-imc/Interpolation_and_SAT-Based_Model_Checking_Revisited.pdf}, institution = {arXiv/CoRR}, month = {August}, }
29. Dirk Beyer, Matthias Dangl, and Philipp Wendler. Combining k-Induction with Continuously-Refined Invariants. Technical report MIP-1503, Department of Computer Science and Mathematics (FIM), University of Passau (PA), January 2015. doi:10.48550/arXiv.1502.00096 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    BibTeX Entry

    @techreport{TR1503-PA15, author = {Dirk Beyer and Matthias Dangl and Philipp Wendler}, title = {Combining k-Induction with Continuously-Refined Invariants}, number = {MIP-1503}, year = {2015}, doi = {10.48550/arXiv.1502.00096}, url = {https://www.sosy-lab.org/research/cpa-k-induction/}, keyword = {CPAchecker,Software Model Checking}, annote = {An <a href="https://www.sosy-lab.org/research/bib/Year/2015.complete.html#CAV15">abbreviated version</a> of this article appeared in Proc. CAV 2015.}, institution = {Department of Computer Science and Mathematics (FIM), University of Passau (PA)}, month = {January}, }
    Additional Infos

    An abbreviated version of this article appeared in Proc. CAV 2015.
30. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Domain-Type-Guided Refinement Selection Based on Sliced Path Prefixes. Technical report MIP-1501, Department of Computer Science and Mathematics (FIM), University of Passau (PA), January 2015. doi:10.48550/arXiv.1502.00045 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    BibTeX Entry

    @techreport{TR1501-PA15, author = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler}, title = {Domain-Type-Guided Refinement Selection Based on Sliced Path Prefixes}, number = {MIP-1501}, year = {2015}, doi = {10.48550/arXiv.1502.00045}, url = {https://www.sosy-lab.org/research/cpa-ref-sel/}, keyword = {CPAchecker,Software Model Checking}, annote = {Extended publications based on this article appeared in <a href="https://www.sosy-lab.org/research/bib/Year/2015.complete.html#FORTE15">Proc. FORTE 2015</a> and <a href="https://www.sosy-lab.org/research/bib/Year/2015.complete.html#SPIN15b">Proc. SPIN 2015</a>.}, institution = {Department of Computer Science and Mathematics (FIM), University of Passau (PA)}, month = {January}, }
    Additional Infos

    Extended publications based on this article appeared in Proc. FORTE 2015 and Proc. SPIN 2015.
31. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Reusing Precisions for Efficient Regression Verification. Technical report MIP-1302, Department of Computer Science and Mathematics (FIM), University of Passau (PA), May 2013. doi:10.48550/arXiv.1305.6915 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems, namely, 59 device drivers with 1119 revisions from the Linux kernel.
    BibTeX Entry

    @techreport{TR1302-PA13, author = {Dirk Beyer and Stefan L{\"o}we and Evgeny Novikov and Andreas Stahlbauer and Philipp Wendler}, title = {Reusing Precisions for Efficient Regression Verification}, number = {MIP-1302}, year = {2013}, doi = {10.48550/arXiv.1305.6915}, url = {https://www.sosy-lab.org/research/cpa-reuse/}, abstract = {Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems, namely, 59 device drivers with 1119 revisions from the Linux kernel.}, keyword = {CPAchecker,Software Model Checking}, annote = {An <a href="https://www.sosy-lab.org/research/bib/Year/2013.complete.html#FSE13">abbreviated version</a> of this article appeared in Proc. ESEC/FSE 2013.}, institution = {Department of Computer Science and Mathematics (FIM), University of Passau (PA)}, month = {May}, }
    Additional Infos

    An abbreviated version of this article appeared in Proc. ESEC/FSE 2013.
32. Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. Feature-Aware Verification. Technical report MIP-1105, Department of Computer Science and Mathematics (FIM), University of Passau (PA), September 2011. doi:10.48550/arXiv.1110.0021 Keyword(s): Software Model Checking Publisher's Version PDF Supplement
    Abstract

    A software product line is a set of software products that are distinguished in terms of features (i.e., end-user-visible units of behavior). Feature interactions -situations in which the combination of features leads to emergent and possibly critical behavior- are a major source of failures in software product lines. We explore how feature-aware verification can improve the automatic detection of feature interactions in software product lines. Feature-aware verification uses product-line verification techniques and supports the specification of feature properties along with the features in separate and composable units. It integrates the technique of variability encoding to verify a product line without generating and checking a possibly exponential number of feature combinations. We developed the tool suite SPLverifier for feature-aware verification, which is based on standard model-checking technology. We applied it to an e-mail system that incorporates domain knowledge of AT&T. We found that feature interactions can be detected automatically based on specifications that have only feature-local knowledge, and that variability encoding significantly improves the verification performance when proving the absence of interactions.
    BibTeX Entry

    @techreport{TR1105-PA11, author = {Sven Apel and Hendrik Speidel and Philipp Wendler and Alexander von Rhein and Dirk Beyer}, title = {Feature-Aware Verification}, number = {MIP-1105}, year = {2011}, doi = {10.48550/arXiv.1110.0021}, url = {http://fosd.net/FAV/}, abstract = {A software product line is a set of software products that are distinguished in terms of features (i.e., end-user--visible units of behavior). Feature interactions ---situations in which the combination of features leads to emergent and possibly critical behavior--- are a major source of failures in software product lines. We explore how feature-aware verification can improve the automatic detection of feature interactions in software product lines. Feature-aware verification uses product-line verification techniques and supports the specification of feature properties along with the features in separate and composable units. It integrates the technique of variability encoding to verify a product line without generating and checking a possibly exponential number of feature combinations. We developed the tool suite SPLverifier for feature-aware verification, which is based on standard model-checking technology. We applied it to an e-mail system that incorporates domain knowledge of AT&T. We found that feature interactions can be detected automatically based on specifications that have only feature-local knowledge, and that variability encoding significantly improves the verification performance when proving the absence of interactions.}, keyword = {Software Model Checking}, annote = {An <a href="https://www.sosy-lab.org/research/bib/Year/2011.complete.html#ASE11">abbreviated version</a> of this article appeared in Proc. ASE 2011.}, institution = {Department of Computer Science and Mathematics (FIM), University of Passau (PA)}, month = {September}, }
    Additional Infos

    An abbreviated version of this article appeared in Proc. ASE 2011.
33. Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, and Philipp Wendler. Conditional Model Checking. Technical report MIP-1107, Department of Computer Science and Mathematics (FIM), University of Passau (PA), September 2011. doi:10.48550/arXiv.1109.6926 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    Abstract

    Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P -usually a state predicate- such that the program satisfies the specification under the condition P -that is, as long as the program does not leave states in which P is satisfied. We are of course interested in model checkers that return conditions P that are as weak as possible. Instead of outcome (1), the model checker will return P = true; instead of (2), the condition P will return the part of the state space that satisfies the specification; and in case (3), the condition P can summarize the work that has been performed by the model checker before space-out, time-out, or giving up. If complete verification is necessary, then a different verification method or tool may be used to focus on the states that violate the condition. We give such conditions as input to a conditional model checker, such that the verification problem is restricted to the part of the state space that satisfies the condition. Our experiments show that repeated application of conditional model checkers, using different conditions, can significantly improve the verification results, state-space coverage, and performance.
    BibTeX Entry

    @techreport{TR1107-PA11, author = {Dirk Beyer and Thomas A. Henzinger and M. Erkan Keremoglu and Philipp Wendler}, title = {Conditional Model Checking}, number = {MIP-1107}, year = {2011}, doi = {10.48550/arXiv.1109.6926}, url = {https://www.sosy-lab.org/~dbeyer/cpa-cmc/}, abstract = {Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave states in which P is satisfied. We are of course interested in model checkers that return conditions P that are as weak as possible. Instead of outcome (1), the model checker will return P = true; instead of (2), the condition P will return the part of the state space that satisfies the specification; and in case (3), the condition P can summarize the work that has been performed by the model checker before space-out, time-out, or giving up. If complete verification is necessary, then a different verification method or tool may be used to focus on the states that violate the condition. We give such conditions as input to a conditional model checker, such that the verification problem is restricted to the part of the state space that satisfies the condition. Our experiments show that repeated application of conditional model checkers, using different conditions, can significantly improve the verification results, state-space coverage, and performance.}, keyword = {CPAchecker,Software Model Checking}, annote = {An <a href="https://www.sosy-lab.org/research/bib/Year/2012.complete.html#FSE12">abbreviated version</a> of this article appeared in Proc. FSE 2012.}, institution = {Department of Computer Science and Mathematics (FIM), University of Passau (PA)}, month = {September}, }
    Additional Infos

    An abbreviated version of this article appeared in Proc. FSE 2012.

34. Philipp Wendler. Towards Practical Predicate Analysis. PhD Thesis, University of Passau, Software Systems Lab, 2017. Keyword(s): Benchmarking, CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
    BibTeX Entry

    @misc{PhilippPredicateAnalysis, author = {Philipp Wendler}, title = {Towards Practical Predicate Analysis}, year = {2017}, url = {https://www.sosy-lab.org/research/phd/wendler/}, pdf = {https://www.sosy-lab.org/research/phd/2017.Wendler.Towards_Practical_Predicate_Analysis.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2017-11-20_RigorosumWendler_TowardsPracticalPredicateAnalysis.pdf}, keyword = {Benchmarking,CPAchecker,Software Model Checking}, annote = {Nominated for the <a href="https://gi.de/aktuelles/wettbewerbe/dissertationspreis/">Dissertation award 2017</a> of the German <a href="https://gi.de/">Gesellschaft f&uuml;r Informatik (GI)</a>}, howpublished = {PhD Thesis, University of Passau, Software Systems Lab}, urn = {urn:nbn:de:bvb:739-opus4-5098}, }
    Additional Infos

    Nominated for the Dissertation award 2017 of the German Gesellschaft für Informatik (GI)
35. Philipp Wendler. Software Verification based on Adjustable Large-Block Encoding. Master's Thesis, University of Passau, Software Systems Lab, 2010. Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry

    @misc{PhilippABE, author = {Philipp Wendler}, title = {Software Verification based on Adjustable Large-Block Encoding}, year = {2010}, pdf = {https://www.sosy-lab.org/research/msc/2010.Wendler.Software_Verification_based_on_Adjustable_Large-Block_Encoding.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems, received for the Faculty Award 2011 for best Master's thesis, and the yearly award of the Chamber of Industry and Commerce of Lower Bavaria (IHK Niederbayern) for an excellent Master's thesis}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
    Additional Infos

    Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems, received for the Faculty Award 2011 for best Master's thesis, and the yearly award of the Chamber of Industry and Commerce of Lower Bavaria (IHK Niederbayern) for an excellent Master's thesis