TACAS presentations on PDR for Software and CPU Energy Meter are available.

Publications about Witness-Based Validation (main)

Articles in conference or workshop proceedings

  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, Part 1, Rhodos, Greece, October 26-30), LNCS 12476, pages 449-470, 2020. Springer. doi:10.1007/978-3-030-61362-4_26 Link to this entry Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry
    @inproceedings{ISoLA20a, 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, Part~1, Rhodos, Greece, October 26-30)}, 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 = {}, abstract = {}, funding = {DFG-CONVEY}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
  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 Link to this entry 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 = {}, funding = {DFG-CONVEY}, isbnnote = {978-3-030-53290-1}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
  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 Link to this entry 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, 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 Link to this entry Keyword(s): CPAchecker, 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,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
  5. 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 Link to this entry 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)}, }
  6. 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 Link to this entry Keyword(s): CPAchecker, 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-FSE15.Witness_Validation_and_Stepwise_Testification_across_Software_Verifiers.pdf}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, }
  7. 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 Link to this entry 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)}, }

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.

Last modified: Mon Apr 19 22:05:36 2021