Publications about Witness-Based Validation
Articles in journal or book chapters
-
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}, }
Articles in conference or workshop proceedings
-
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}, } -
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}, } -
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)}, } -
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}, } -
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. -
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)}, } -
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)}, } -
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}, } -
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. -
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)}, } -
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}, } -
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)}, }
Theses and projects (PhD, MSc, BSc, Project)
-
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}, } -
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}, }
Disclaimer:
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.