Software and Computational Systems Lab

Publications of Matthias Dangl

1. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Thomas Lemberger, and Michael Tautschnig. Verification Witnesses. ACM Trans. Softw. Eng. Methodol., 31(4):57:1-57:69, 2022. doi:10.1145/3477579 Keyword(s): CPAchecker, Ultimate, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Publisher's Version PDF Supplement
   BibTeX Entry

   @article{Witnesses-TOSEM, author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann and Thomas Lemberger and Michael Tautschnig}, title = {Verification Witnesses}, journal = {ACM Trans. Softw. Eng. Methodol.}, volume = {31}, number = {4}, pages = {57:1-57:69}, year = {2022}, doi = {10.1145/3477579}, url = {https://www.sosy-lab.org/research/verification-witnesses-tosem/}, keyword = {CPAchecker,Ultimate,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, _pdf = {https://www.sosy-lab.org/research/pub/2022-TOSEM.Verification_Witnesses.pdf}, _sha256 = {48acf3f35251df635e829b29fe8f16fd50498f8f99a082b8b9e0aa094a97a432}, }
2. 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/

3. Dirk Beyer and Matthias Dangl. Software Verification with PDR: An Implementation of the State of the Art. 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 1, LNCS 12078, pages 3-21, 2020. Springer. doi:10.1007/978-3-030-45190-5_1 Keyword(s): Software Model Checking, CPAchecker Publisher's Version PDF Presentation Video Supplement
   BibTeX Entry

   @inproceedings{TACAS20a, author = {Dirk Beyer and Matthias Dangl}, title = {Software Verification with {PDR}: An Implementation of the State of the Art}, 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 1}, pages = {3-21}, year = {2020}, series = {LNCS~12078}, publisher = {Springer}, doi = {10.1007/978-3-030-45190-5_1}, sha256 = {fbd54433b42cb4411ddf6d73eb198507a6d35d8b6581b000be30aed84633e204}, url = {https://www.sosy-lab.org/research/pdr-compare/}, presentation = {https://www.sosy-lab.org/research/prs/2021-03-31_TACAS20_PDR-for-Software_Dirk.pdf}, abstract = {}, keyword = {Software Model Checking,CPAchecker}, video = {https://youtu.be/Wxqd92sdHBE}, }
4. Dirk Beyer and Matthias Dangl. Strategy Selection for Software Verification Based on Boolean Features: A Simple but Effective Approach. In T. Margaria and B. Steffen, editors, Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2018, Part 2, Limassol, Cyprus, November 5-9), LNCS 11245, pages 144-159, 2018. Springer. doi:10.1007/978-3-030-03421-4_11 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation
   BibTeX Entry

   @inproceedings{ISoLA18a, author = {Dirk Beyer and Matthias Dangl}, title = {Strategy Selection for Software Verification Based on Boolean Features: A Simple but Effective Approach}, booktitle = {Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2018, Part~2, Limassol, Cyprus, November 5-9)}, editor = {T.~Margaria and B.~Steffen}, pages = {144-159}, year = {2018}, series = {LNCS~11245}, publisher = {Springer}, doi = {10.1007/978-3-030-03421-4_11}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2018-ISoLA.Strategy_Selection_for_Software_Verification_Based_on_Boolean_Features.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-11-05_ISoLA18_StrategySelection_Dirk.pdf}, keyword = {CPAchecker,Software Model Checking}, }
5. Dirk Beyer, Matthias Dangl, Thomas Lemberger, and Michael Tautschnig. Tests from Witnesses: Execution-Based Validation of Verification Results. In Catherine Dubois and Burkhart Wolff, editors, Proceedings of the 12th International Conference on Tests and Proofs (TAP 2018, Toulouse, France, June 27-29), LNCS 10889, pages 3-23, 2018. Springer. doi:10.1007/978-3-319-92994-1_1 Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Publisher's Version PDF Presentation Supplement
   Abstract

   The research community made enormous progress in the past years in developing algorithms for verifying software, as shown by verification competitions (SV-COMP). However, the ultimate goal is to design certifying algorithms, which produce for a given input not only the output but in addition a witness. This makes it possible to validate that the output is a correct solution for the input problem. The advantage of certifying algorithms is that the validation of the result is —thanks to the witness— easier than the computation of the result. Unfortunately, the transfer to industry is slow, one of the reasons being that some verifiers report a considerable number of false alarms. The verification community works towards this ultimate goal using exchangeable violation witnesses, i.e., an independent validator can be used to check whether the produced witness indeed represents a bug. This reduces the required trust base from the complex verification tool to a validator that may be less complex, and thus, more easily trustable. But existing witness validators are based on model-checking technology — which does not solve the problem of reducing the trust base. To close this gap, we present a simple concept that is based on program execution: We extend witness validation by generating a test vector from an error path that is reconstructed from the witness. Then, we generate a test harness (similar to unit-test code) that can be compiled and linked together with the original program. We then run the executable program in an isolating container. If the execution violates the specification (similar to runtime verification) we confirm that the witness indeed represents a bug. This method reduces the trust base to the execution system, which seems appropriate for avoiding false alarms. To show feasibility and practicality, we implemented execution-based witness validation in two completely independent analysis frameworks, and performed a large experimental study.
   BibTeX Entry

   @inproceedings{TAP18, author = {Dirk Beyer and Matthias Dangl and Thomas Lemberger and Michael Tautschnig}, title = {Tests from Witnesses: Execution-Based Validation of Verification Results}, booktitle = {Proceedings of the 12th International Conference on Tests and Proofs (TAP~2018, Toulouse, France, June 27-29)}, editor = {Catherine Dubois and Burkhart Wolff}, pages = {3-23}, year = {2018}, series = {LNCS~10889}, publisher = {Springer}, doi = {10.1007/978-3-319-92994-1_1}, sha256 = {}, url = {https://www.sosy-lab.org/research/tests-from-witnesses/}, pdf = {https://www.sosy-lab.org/research/pub/2018-TAP.Tests_from_Witnesses_Execution-Based_Validation_of_Verification_Results.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-06-27_TAP18-Keynote-CooperativeVerification_Dirk.pdf}, abstract = {The research community made enormous progress in the past years in developing algorithms for verifying software, as shown by verification competitions (SV-COMP). However, the ultimate goal is to design certifying algorithms, which produce for a given input not only the output but in addition a witness. This makes it possible to validate that the output is a correct solution for the input problem. The advantage of certifying algorithms is that the validation of the result is —thanks to the witness— easier than the computation of the result. Unfortunately, the transfer to industry is slow, one of the reasons being that some verifiers report a considerable number of false alarms. The verification community works towards this ultimate goal using exchangeable violation witnesses, i.e., an independent validator can be used to check whether the produced witness indeed represents a bug. This reduces the required trust base from the complex verification tool to a validator that may be less complex, and thus, more easily trustable. But existing witness validators are based on model-checking technology — which does not solve the problem of reducing the trust base. To close this gap, we present a simple concept that is based on program execution: We extend witness validation by generating a test vector from an error path that is reconstructed from the witness. Then, we generate a test harness (similar to unit-test code) that can be compiled and linked together with the original program. We then run the executable program in an isolating container. If the execution violates the specification (similar to runtime verification) we confirm that the witness indeed represents a bug. This method reduces the trust base to the execution system, which seems appropriate for avoiding false alarms. To show feasibility and practicality, we implemented execution-based witness validation in two completely independent analysis frameworks, and performed a large experimental study.}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
6. Dirk Beyer, Matthias Dangl, Daniel Dietsch, and Matthias Heizmann. Exchanging Verification Witnesses between Verifiers. In J. Jürjens and K. Schneider, editors, Tagungsband Software Engineering 2017, Fachtagung des GI-Fachbereichs Softwaretechnik (21.-24. Februar 2017, Hannover, Deutschland), LNI P-267, pages 93-94, 2017. Gesellschaft für Informatik (GI). Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation Publisher's Version
   BibTeX Entry

   @inproceedings{SE17-Witnesses, author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann}, title = {Exchanging Verification Witnesses between Verifiers}, booktitle = {Tagungsband Software Engineering 2017, Fachtagung des GI-Fachbereichs Softwaretechnik (21.-24. Februar 2017, Hannover, Deutschland)}, editor = {J.~J{\"{u}}rjens and K.~Schneider}, pages = {93-94}, year = {2017}, series = {{LNI}~P-267}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, url = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2016.html#FSE16b">full article on this topic</a> that appeared in Proc. ESEC/FSE 2016.}, doinone = {DOI not available}, urlpub = {https://dl.gi.de/handle/20.500.12116/1288}, }
   Additional Infos

   This is a summary of a full article on this topic that appeared in Proc. ESEC/FSE 2016.
7. Dirk Beyer, Matthias Dangl, Daniel Dietsch, and Matthias Heizmann. Correctness Witnesses: Exchanging Verification Results Between Verifiers. In T. Zimmermann, J. Cleland-Huang, and Z. Su, editors, Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016, Seattle, WA, USA, November 13-18), pages 326-337, 2016. ACM. doi:10.1145/2950290.2950351 Keyword(s): CPAchecker, Ultimate, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Publisher's Version PDF
   BibTeX Entry

   @inproceedings{FSE16b, author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann}, title = {Correctness Witnesses: {E}xchanging Verification Results Between Verifiers}, booktitle = {Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE~2016, Seattle, WA, USA, November 13-18)}, editor = {T.~Zimmermann and J.~Cleland-Huang and Z.~Su}, pages = {326-337}, year = {2016}, publisher = {ACM}, doi = {10.1145/2950290.2950351}, sha256 = {}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2016-FSE.Correctness_Witnesses_Exchanging_Verification_Results_between_Verifiers.pdf}, keyword = {CPAchecker,Ultimate,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
8. Dirk Beyer and Matthias Dangl. Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses. In S. Chaudhuri and A. Farzan, editors, 28th International Conference on Computer Aided Verification (CAV 2016, Part 2, Toronto, ON, Canada, July 17-23), LNCS 9780, pages 502-509, 2016. Springer. doi:10.1007/978-3-319-41540-6_28 Keyword(s): Cloud-Based Software Verification, Witness-Based Validation, Witness-Based Validation (main) Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CAV16, author = {Dirk Beyer and Matthias Dangl}, title = {Verification-Aided Debugging: {A}n Interactive Web-Service for Exploring Error Witnesses}, booktitle = {28th International Conference on Computer Aided Verification (CAV~2016, Part~2, Toronto, ON, Canada, July 17-23)}, editor = {S.~Chaudhuri and A.~Farzan}, pages = {502-509}, year = {2016}, series = {LNCS~9780}, publisher = {Springer}, doi = {10.1007/978-3-319-41540-6_28}, sha256 = {89a353eace6233e10cd85e64b0c197209367d617b94c2d02766e922ea88c9e4c}, pdf = {https://www.sosy-lab.org/research/pub/2016-CAV.Verification-Aided_Debugging_An_Interactive_Web-Service_for_Exploring_Error_Witnesses.pdf}, keyword = {Cloud-Based Software Verification,Witness-Based Validation,Witness-Based Validation (main)}, }
9. Dirk Beyer and Matthias Dangl. SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms. In Proc. VSTTE, LNCS 9971, pages 181-198, 2016. Springer. doi:10.1007/978-3-319-48869-1_14 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{VSTTE16b-AlgorithmComparison, author = {Dirk Beyer and Matthias Dangl}, title = {{SMT}-based Software Model Checking: {A}n Experimental Comparison of Four Algorithms}, booktitle = {Proc.\ VSTTE}, pages = {181--198}, year = {2016}, series = {LNCS~9971}, publisher = {Springer}, doi = {10.1007/978-3-319-48869-1_14}, sha256 = {}, url = {https://www.sosy-lab.org/research/k-ind-compare/index-vstte.html}, pdf = {https://www.sosy-lab.org/research/pub/2016-VSTTE.SMT-based_Software_Model_Checking_An_Experimental_Comparison_of_Four_Algorithms.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {An <a href="https://www.sosy-lab.org/research/bib/Year/2018.complete.html#AlgorithmComparison-JAR">extended version</a> of this article appeared in JAR.}, }
   Additional Infos

   An extended version of this article appeared in JAR.
10. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, and Andreas Stahlbauer. Verification Witnesses. In J. Knoop and U. Zdun, editors, Tagungsband Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik (23.-26. Februar 2016, Wien, Österreich), LNI 252, pages 105-106, 2016. Gesellschaft für Informatik (GI). Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation Publisher's Version
    BibTeX Entry

    @inproceedings{SE16b-VerificationWitnesses, author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann and Andreas Stahlbauer}, title = {Verification Witnesses}, booktitle = {Tagungsband Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik (23.-26. Februar 2016, Wien, {\"O}sterreich)}, editor = {J.~Knoop and U.~Zdun}, pages = {105-106}, year = {2016}, series = {{LNI}~252}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, url = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation}, annote = {This is a summary of a <a href="https://www.sosy-lab.org/research/bib/Year/2015.html#FSE15">full article on this topic</a> that appeared in Proc. ESEC/FSE 2015.}, doinone = {DOI not available}, urlpub = {https://dl.gi.de/handle/20.500.12116/746}, }
    Additional Infos

    This is a summary of a full article on this topic that appeared in Proc. ESEC/FSE 2015.
11. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, and Andreas Stahlbauer. Witness Validation and Stepwise Testification across Software Verifiers. In E. Di Nitto, M. Harman, and P. Heymans, editors, Proceedings of the 2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2015, Bergamo, Italy, August 31 - September 4), pages 721-733, 2015. ACM, New York. doi:10.1145/2786805.2786867 Keyword(s): CPAchecker, Ultimate, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Publisher's Version PDF
    BibTeX Entry

    @inproceedings{FSE15, author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann and Andreas Stahlbauer}, title = {Witness Validation and Stepwise Testification across Software Verifiers}, booktitle = {Proceedings of the 2015 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2015, Bergamo, Italy, August 31 - September 4)}, editor = {E.~Di~Nitto and M.~Harman and P.~Heymans}, pages = {721-733}, year = {2015}, publisher = {ACM, New York}, isbn = {978-1-4503-3675-8}, doi = {10.1145/2786805.2786867}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2015-FSE.Witness_Validation_and_Stepwise_Testification_across_Software_Verifiers.pdf}, keyword = {CPAchecker,Ultimate,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
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. 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

14. Dirk Beyer and Matthias Dangl. Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art. Technical report 1908.06271, arXiv/CoRR, August 2019. doi:10.48550/arXiv.1908.06271 Publisher's Version PDF
    BibTeX Entry

    @techreport{TechReport19b, author = {Dirk Beyer and Matthias Dangl}, title = {Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art}, number = {1908.06271}, year = {2019}, doi = {10.48550/arXiv.1908.06271}, institution = {arXiv/CoRR}, month = {August}, }
15. 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.

16. Matthias Dangl. Witness-Based Validation of Verification Results with Applications to Software-Model Checking. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.31508 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
    BibTeX Entry

    @misc{DanglWitnesses, author = {Matthias Dangl}, title = {Witness-Based Validation of Verification Results with Applications to Software-Model Checking}, year = {2022}, doi = {10.5282/edoc.31508}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/31508/3/Dangl_Matthias.pdf}, presentation = {}, keyword = {CPAchecker,Software Model Checking}, annote = {Now at ARS, Munich, Germany}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-315089}, }
    Additional Infos

    Now at ARS, Munich, Germany
17. Matthias Dangl. Light-Weight Invariant Generation for Software Verification with CPAchecker. Master's Thesis, University of Passau, Software Systems Lab, 2013. Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry

    @misc{MatthiasInvariantGeneration, author = {Matthias Dangl}, title = {Light-Weight Invariant Generation for Software Verification with {{\sc CPAchecker}}}, year = {2013}, pdf = {https://www.sosy-lab.org/research/msc/2015.Dangl.Light-Weight_Invariant_Generation_for_Software_Verification_with_CPAchecker.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }