Software and Computational Systems Lab

Publications about Witness-Based Validation

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}, }

1. Dirk Beyer and Karlheinz Friedberger. Violation Witnesses and Result Validation for Multi-Threaded Programs. In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodos, Greece, October 26-30), part 1, LNCS 12476, pages 449-470, 2020. Springer. doi:10.1007/978-3-030-61362-4_26 Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
   BibTeX Entry

   @inproceedings{ISoLA20c, author = {Dirk Beyer and Karlheinz Friedberger}, title = {Violation Witnesses and Result Validation for Multi-Threaded Programs}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodos, Greece, October 26-30), part~1}, editor = {T.~Margaria and B.~Steffen}, pages = {449-470}, year = {2020}, series = {LNCS~12476}, publisher = {Springer}, doi = {10.1007/978-3-030-61362-4_26}, sha256 = {65fc5325c4e77a80d8e47f9c0e7f0ac02379bfa15dcd9fb54d6587185b8efd77}, url = {https://www.sosy-lab.org/research/witnesses-concurrency/}, presentation = {https://www.sosy-lab.org/research/prs/2021-10-25_ISOLA21_ValidationMultiThreaded_Dirk.pdf}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, funding = {DFG-CONVEY}, }
2. Dirk Beyer and Martin Spiessl. MetaVal: Witness Validation via Verification. In S. K. Lahiri and C. Wang, editors, Proceedings of the 32nd International Conference on Computer Aided Verification (CAV 2020, Virtual, USA, July 21-24), part 2, LNCS 12225, pages 165-177, 2020. Springer. doi:10.1007/978-3-030-53291-8_10 Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Funding: DFG-CONVEY Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{CAV20, author = {Dirk Beyer and Martin Spiessl}, title = {MetaVal: {W}itness Validation via Verification}, booktitle = {Proceedings of the 32nd International Conference on Computer Aided Verification (CAV~2020, Virtual, USA, July 21-24), part 2}, editor = {S.~K.~Lahiri and C.~Wang}, pages = {165-177}, year = {2020}, series = {LNCS~12225}, publisher = {Springer}, doi = {10.1007/978-3-030-53291-8_10}, sha256 = {7431085a248c7e2cab70318096622ff19ce1124067158d08866d3f9b250df44e}, url = {https://gitlab.com/sosy-lab/software/metaval}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, funding = {DFG-CONVEY}, isbnnote = {978-3-030-53290-1}, }
3. 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)}, }
4. Dirk Beyer. Software Verification with Validation of Results (Report on SV-COMP 2017). In A. Legay and T. Margaria, editors, Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017, Uppsala, Sweden, April 22-29), LNCS 10206, pages 331-349, 2017. Springer-Verlag, Heidelberg. doi:10.1007/978-3-662-54580-5_20 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking, Witness-Based Validation Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{TACAS17, author = {Dirk Beyer}, title = {Software Verification with Validation of Results ({R}eport on {SV-COMP} 2017)}, booktitle = {Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2017, Uppsala, Sweden, April 22-29)}, editor = {A.~Legay and T.~Margaria}, pages = {331-349}, year = {2017}, series = {LNCS~10206}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-662-54579-9}, doi = {10.1007/978-3-662-54580-5_20}, sha256 = {}, url = {https://sv-comp.sosy-lab.org/2017/}, pdf = {https://www.sosy-lab.org/research/pub/2017-TACAS.Software_Verification_with_Validation_of_Results.pdf}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking,Witness-Based Validation}, }
5. 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.
6. 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)}, }
7. 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)}, }
8. Dirk Beyer. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). In M. Chechik and J.-F. Raskin, editors, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016, Eindhoven, The Netherlands, April 2-8), LNCS 9636, pages 887-904, 2016. Springer-Verlag, Heidelberg. doi:10.1007/978-3-662-49674-9_55 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking, Witness-Based Validation Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{TACAS16, author = {Dirk Beyer}, title = {Reliable and Reproducible Competition Results with {{\sc BenchExec}} and Witnesses ({R}eport on {SV-COMP} 2016)}, booktitle = {Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2016, Eindhoven, The Netherlands, April 2-8)}, editor = {M.~Chechik and J.-F.~Raskin}, pages = {887-904}, year = {2016}, series = {LNCS~9636}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-662-49674-9}, doi = {10.1007/978-3-662-49674-9_55}, sha256 = {bc8f02d7c0651c1197977f13e77c1fcb22a5f85aadd96dc4aa59b454b199ed0e}, url = {https://sv-comp.sosy-lab.org/2016/}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking,Witness-Based Validation}, }
9. 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.
10. 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)}, }
11. Dirk Beyer. Software Verification and Verifiable Witnesses (Report on SV-COMP 2015). 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 401-416, 2015. Springer-Verlag, Heidelberg. doi:10.1007/978-3-662-46681-0_31 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking, Witness-Based Validation Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{TACAS15, author = {Dirk Beyer}, title = {Software Verification and Verifiable Witnesses (Report on {SV-COMP} 2015)}, 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 = {401-416}, year = {2015}, series = {LNCS~9035}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-662-46680-3}, doi = {10.1007/978-3-662-46681-0_31}, sha256 = {858448ee22256b3ed7f35603d81e942b58652f3b4d2660a22b858dc1c3ac16d0}, url = {https://sv-comp.sosy-lab.org/2015/}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking,Witness-Based Validation}, }
12. 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)}, }

1. Maximilian Wiesholler. Correctness Witness Validation using Predicate Analysis. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2019. Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation PDF Presentation
   BibTeX Entry

   @misc{WieshollerWitnesses, author = {Maximilian Wiesholler}, title = {Correctness Witness Validation using Predicate Analysis}, year = {2019}, pdf = {https://www.sosy-lab.org/research/bsc/2019.Wiesholler.Correctness_Witness_Validation_using_Predicate_Analysis.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-06-05_BA_CorrectnessWitnessValidationUsingPredicateAnalysis_Wiesholler.pdf}, keyword = {CPAchecker, Software Model Checking, Witness-Based Validation}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
2. Nicholas Reyes. Integrating a Witness Store into a Distributed Verification System. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): Witness-Based Validation, Cloud-Based Software Verification
   BibTeX Entry

   @misc{ReyesWitnessStore, author = {Nicholas Reyes}, title = {Integrating a Witness Store into a Distributed Verification System}, year = {2018}, keyword = {Witness-Based Validation,Cloud-Based Software Verification}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }