Publications
Publications by year
2022
-
Verification Witnesses.
ACM Trans. Softw. Eng. Methodol.,
2022.
PDF
Supplement
BibTeX Entry
@article{WitnessesACM, author = {D.~Beyer and M.~Dangl and D.~Dietsch and M.~Heizmann and T.~Lemberger and M.~Tautschnig}, title = {Verification Witnesses}, journal = {ACM Trans. Softw. Eng. Methodol.}, year = {2022}, url = {https://www.sosy-lab.org/research/verification-witnesses-tosem/}, pdf = {https://www.sosy-lab.org/research/pub/2022-TOSEM.Verification_Witnesses.pdf}, doinone = {10.1145/3477579}, } -
Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR.
In Proceedings of the 44th International Conference on
Software Engineering (ICSE 2022, Pittsburgh, PA, USA, May 8-20 (Virtual), May 22-27 (In-Person)),
2022.
ACM.
Funding:
DFG-COOP
PDF
Supplement
Artifact(s)
Abstract
Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components. In this paper, we propose to strictly decompose software verification: the verification task is split into independent subtasks, implemented by only loosely coupled components communicating via clearly defined interfaces. We apply this decomposition concept to one of the most frequently employed techniques in software verification: counterexample-guided abstraction refinement (CEGAR). CEGAR is a technique to iteratively compute an abstract model of the system. We develop a decomposition of CEGAR into independent components with clearly defined interfaces that are based on existing, standardized exchange formats. Its realization component-based CEGAR (C-CEGAR) concerns the three core tasks of CEGAR: abstract-model exploration, feasibility check, and precision refinement. We experimentally show that - despite the necessity of exchanging complex data via interfaces - the efficiency thereby only reduces by a small constant factor while the precision in solving verification tasks even increases. We furthermore illustrate the advantages of C-CEGAR by experimenting with different implementations of components, thereby further increasing the overall effectiveness and testing that substitution of components works well.BibTeX Entry
@inproceedings{ICSE22, author = {Dirk Beyer and Jan Haltermann and Thomas Lemberger and Heike Wehrheim}, title = {Decomposing Software Verification into Off-the-Shelf Components: An Application to {CEGAR}}, booktitle = {Proceedings of the 44th International Conference on Software Engineering (ICSE~2022, Pittsburgh, PA, USA, May 8-20 (Virtual), May 22-27 (In-Person))}, year = {2022}, publisher = {ACM}, url = {https://www.sosy-lab.org/research/component-based-cegar/}, pdf = {https://www.sosy-lab.org/research/pub/2022-ICSE.Decomposing_Software_Verification_into_Off-the-Shelf-Components.pdf}, abstract = {Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components. In this paper, we propose to strictly decompose software verification: the verification task is split into independent subtasks, implemented by only loosely coupled components communicating via clearly defined interfaces. We apply this decomposition concept to one of the most frequently employed techniques in software verification: counterexample-guided abstraction refinement (CEGAR). CEGAR is a technique to iteratively compute an abstract model of the system. We develop a decomposition of CEGAR into independent components with clearly defined interfaces that are based on existing, standardized exchange formats. Its realization component-based CEGAR (C-CEGAR) concerns the three core tasks of CEGAR: abstract-model exploration, feasibility check, and precision refinement. We experimentally show that --- despite the necessity of exchanging complex data via interfaces --- the efficiency thereby only reduces by a small constant factor while the precision in solving verification tasks even increases. We furthermore illustrate the advantages of C-CEGAR by experimenting with different implementations of components, thereby further increasing the overall effectiveness and testing that substitution of components works well.}, artifact = {10.5281/zenodo.5301636}, doinone = {Unpublished: Last checked: 2022-02-19}, funding = {DFG-COOP}, } -
The Static Analyzer Infer in SV-COMP (Competition Contribution).
In Proceedings of the 28th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2022, Munich, Germany, April 2-7), Part 2,
LNCS 13244,
2022.
Springer.
PDF
Abstract
We present Infer-SV, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-SV, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.BibTeX Entry
@inproceedings{INFER-SVCOMP22, author = {Matthias Kettl and Thomas Lemberger}, title = {The Static Analyzer Infer in {SV-COMP} (Competition Contribution)}, booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7), Part 2}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2022-SVCOMP.The_Static_Analyzer_Infer_in_SV-COMP.pdf}, abstract = {We present Infer-SV, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-SV, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.}, doinone = {Unpublished: Last checked: 2022-01-03}, }
2021
-
Towards a Benchmark Set for Program Repair Based on Partial Fixes.
Technical report 2107.08038, arXiv/CoRR,
July
2021.
PDF
BibTeX Entry
@techreport{TechReport21a, author = {Dirk Beyer and Lars Grunske and Thomas Lemberger and Minxing Tang}, title = {Towards a Benchmark Set for Program Repair Based on Partial Fixes}, number = {2107.08038}, year = {2021}, pdf = {https://arxiv.org/abs/2107.08038}, institution = {arXiv/CoRR}, month = {July}, }
2020
-
Plain random test generation with PRTest.
International Journal on Software Tools for Technology Transfer (STTT),
2020.
Springer.
doi:10.1007/s10009-020-00568-x
Publisher's Version
PDF
Presentation
Abstract
Automatic test-suite generation tools are often complex and their behavior is not predictable. To provide a minimum baseline that test-suite generators should be able to surpass, we present PRTest, a random black-box test-suite generator for C programs: To create a test, PRTest natively executes the program under test and creates a new, random test value whenever an input value is required. After execution, PRTest checks whether any new program branches were covered and, if this is the case, the created test is added to the test suite. This way, tests are rapidly created either until a crash is found, or until the user aborts the creation. While this naive mechanism is not competitive with more sophisticated, state-of-the-art test-suite generation tools, it is able to provide a good baseline for Test-Comp and a fast alternative for automatic test-suite generation for programs with simple control flow. PRTest is publicly available and open source.BibTeX Entry
@article{PRTEST19, author = {Thomas Lemberger}, title = {Plain random test generation with {PRTest}}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {}, number = {}, pages = {}, year = {2020}, publisher = {Springer}, doi = {10.1007/s10009-020-00568-x}, sha256 = {2e5ae7091b6adb758c123dfe62d3fab57203f930883539beb20f6e91391ebc77}, pdf = {https://www.sosy-lab.org/research/pub/2020-STTT.Plain_random_test_generation_with_PRTest.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-04-06_TestComp19_PRTest_Thomas.pdf}, abstract = {Automatic test-suite generation tools are often complex and their behavior is not predictable. To provide a minimum baseline that test-suite generators should be able to surpass, we present PRTest, a random black-box test-suite generator for C programs: To create a test, PRTest natively executes the program under test and creates a new, random test value whenever an input value is required. After execution, PRTest checks whether any new program branches were covered and, if this is the case, the created test is added to the test suite. This way, tests are rapidly created either until a crash is found, or until the user aborts the creation. While this naive mechanism is not competitive with more sophisticated, state-of-the-art test-suite generation tools, it is able to provide a good baseline for Test-Comp and a fast alternative for automatic test-suite generation for programs with simple control flow. PRTest is publicly available and open source.}, annote = {Publication appeared first online in July 2020.
PRTest is available at https://gitlab.com/sosy-lab/software/prtest}, }Additional Infos
Publication appeared first online in July 2020.
PRTest is available at https://gitlab.com/sosy-lab/software/prtest -
Difference Verification with Conditions.
In Proceedings of the 18th International Conference on
Software Engineering and Formal Methods (SEFM 2020, Virtual, Netherlands, September 14-18),
LNCS 12310,
pages 133-154,
2020.
Springer.
doi:10.1007/978-3-030-58768-0_8
Funding:
DFG-COOP,
DFG-CONVEY
Publisher's Version
PDF
Presentation
Video
Supplement
Abstract
Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.BibTeX Entry
@inproceedings{SEFM20b, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger}, title = {Difference Verification with Conditions}, booktitle = {Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18)}, pages = {133–154}, year = {2020}, series = {LNCS~12310}, publisher = {Springer}, doi = {10.1007/978-3-030-58768-0_8}, sha256 = {8e5219da9a998b26f59013c809fbb1db6f92e3f08125fa1bfaacafcfafafef7f}, url = {https://www.sosy-lab.org/research/difference/}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-17_SEFM20_DifferenceVerificationWithConditions_Thomas.pdf}, abstract = {Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.}, funding = {DFG-COOP,DFG-CONVEY}, isbnnote = {}, video = {https://youtu.be/dG02602c9oo}, }
2019
-
Combining Verifiers in Conditional Model Checking via Reducers.
In Proceedings of the Conference on
Software Engineering and Software Management (SE/SWM 2019, Stuttgart, Germany, February 18-22),
LNI P-292,
pages 151-152,
2019.
GI.
doi:10.18420/se2019-46
Publisher's Version
PDF
Presentation
Abstract
Software verification received lots of attention in the past two decades. Nonetheless, it remains an extremely difficult problem. Some verification tasks cannot be solved automatically by any of today’s verifiers. To still verify such tasks, one can combine the strengths of different verifiers. A promising approach to create combinations is conditional model checking (CMC). In CMC, the first verifier outputs a condition that describes the parts of the program state space that it successfully verified, and the next verifier uses that condition to steer its exploration towards the unverified state space. Despite the benefits of CMC, only few verifiers can handle conditions. To overcome this problem, we propose an automatic plug-and-play extension for verifiers. Instead of modifying verifiers, we suggest to add a preprocessor: the reducer. The reducer takes the condition and the original program and computes a residual program that encodes the unverified state space in program code. We developed one such reducer and use it to integrate existing verifiers and test-case generators into the CMC process. Our experiments show that we can solve many additional verification tasks with this reducer-based construction.BibTeX Entry
@inproceedings{SE19, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger and Heike Wehrheim}, title = {Combining Verifiers in Conditional Model Checking via Reducers}, booktitle = {Proceedings of the Conference on Software Engineering and Software Management (SE/SWM~2019, Stuttgart, Germany, February 18-22)}, pages = {151–152}, year = {2019}, series = {{LNI}~P-292}, publisher = {{GI}}, doi = {10.18420/se2019-46}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2019-SE.Combining_Verifiers_in_Conditional_Model_Checking_via_Reducers.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-02-22_SE19_CombiningVerifiersInConditionalModelChecking_Marie.pdf}, abstract = {Software verification received lots of attention in the past two decades. Nonetheless, it remains an extremely difficult problem. Some verification tasks cannot be solved automatically by any of today’s verifiers. To still verify such tasks, one can combine the strengths of different verifiers. A promising approach to create combinations is conditional model checking (CMC). In CMC, the first verifier outputs a condition that describes the parts of the program state space that it successfully verified, and the next verifier uses that condition to steer its exploration towards the unverified state space. Despite the benefits of CMC, only few verifiers can handle conditions. To overcome this problem, we propose an automatic plug-and-play extension for verifiers. Instead of modifying verifiers, we suggest to add a preprocessor: the reducer. The reducer takes the condition and the original program and computes a residual program that encodes the unverified state space in program code. We developed one such reducer and use it to integrate existing verifiers and test-case generators into the CMC process. Our experiments show that we can solve many additional verification tasks with this reducer-based construction.}, annote = {This is a summary of a full article on this topic that appeared in Proc. ICSE 2018.}, }Additional Infos
This is a summary of a full article on this topic that appeared in Proc. ICSE 2018. -
TestCov: Robust Test-Suite Execution and Coverage Measurement.
In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019, San Diego, CA, USA, November 11-15),
pages 1074-1077,
2019.
IEEE.
doi:10.1109/ASE.2019.00105
Funding:
DFG-COOP
Publisher's Version
PDF
Presentation
BibTeX Entry
@inproceedings{ASE19, author = {Dirk Beyer and Thomas Lemberger}, title = {{T}est{C}ov: Robust Test-Suite Execution and Coverage Measurement}, booktitle = {Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019, San Diego, CA, USA, November 11-15)}, pages = {1074-1077}, year = {2019}, publisher = {IEEE}, doi = {10.1109/ASE.2019.00105}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2019-ASE.TestCov_Robust_Test-Suite_Execution_and_Coverage_Measurement.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-11-12_ASE19_TestCov_Thomas_Lemberger.pdf}, funding = {DFG-COOP}, isbnnote = {978-1-7281-2508-4}, } -
Conditional Testing - Off-the-Shelf Combination of Test-Case Generators.
In Proceedings of the 17th International Symposium on
Automated Technology for Verification and Analysis (ATVA 2019, Taipei, Taiwan, October 28-31),
LNCS 11781,
pages 189-208,
2019.
Springer.
doi:10.1007/978-3-030-31784-3_11
Funding:
DFG-COOP
Publisher's Version
PDF
Presentation
Supplement
BibTeX Entry
@inproceedings{ATVA19, author = {Dirk Beyer and Thomas Lemberger}, title = {Conditional Testing - Off-the-Shelf Combination of Test-Case Generators}, booktitle = {Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA~2019, Taipei, Taiwan, October 28-31)}, pages = {189-208}, year = {2019}, series = {LNCS~11781}, publisher = {Springer}, doi = {10.1007/978-3-030-31784-3_11}, sha256 = {}, url = {https://www.sosy-lab.org/research/conditional-testing/}, pdf = {https://www.sosy-lab.org/research/pub/2019-ATVA.Conditional_Testing_Off-the-Shelf_Combination_of_Test-Case_Generators.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2019-10-29_ATVA19_Conditional_Testing_Thomas_Lemberger.pdf}, funding = {DFG-COOP}, }
2018
-
CPA-SymExec: Efficient Symbolic Execution in CPAchecker.
In Proceedings of the 33rd ACM/IEEE International Conference on Automated
Software Engineering (ASE 2018, Montpellier, France, September 3-7),
pages 900-903,
2018.
ACM.
doi:10.1145/3238147.3240478
Publisher's Version
PDF
Presentation
Video
Supplement
Abstract
We present CPA-SymExec, a tool for symbolic execution that is implemented in the open-source, configurable verification framework CPAchecker. Our implementation automatically detects which symbolic facts to track, in order to obtain a small set of constraints that are necessary to decide reachability of a program area of interest. CPA-SymExec is based on abstraction and counterexample-guided abstraction refinement (CEGAR), and uses a constraint-interpolation approach to detect symbolic facts. We show that our implementation can better mitigate the path-explosion problem than symbolic execution without abstraction, by comparing the performance to the state-of-the-art Klee-based symbolic-execution engine Symbiotic and to Klee itself. For the experiments we use two kinds of analysis tasks: one for finding an executable path to a specific location of interest (e.g., if a test vector is desired to show that a certain behavior occurs), and one for confirming that no executable path to a specific location exists (e.g., if it is desired to show that a certain behavior never occurs). CPA-SymExec is released under the Apache 2 license and available (inclusive source code) at https://cpachecker.sosy-lab.org. A demonstration video is available at https://youtu.be/qoBHtvPKtnw.BibTeX Entry
@inproceedings{ASE18b, author = {Dirk Beyer and Thomas Lemberger}, title = {{CPA-SymExec}: Efficient Symbolic Execution in {CPAchecker}}, booktitle = {Proceedings of the 33rd {ACM/IEEE} International Conference on Automated Software Engineering ({ASE}~2018, Montpellier, France, September 3-7)}, pages = {900-903}, year = {2018}, publisher = {ACM}, doi = {10.1145/3238147.3240478}, sha256 = {}, url = {https://www.sosy-lab.org/research/cpa-symexec-tool/}, pdf = {https://www.sosy-lab.org/research/pub/2018-ASE.CPA-SymExec_Efficient_Symbolic_Execution_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-09-07_ASE18_CPASymExec_Thomas.pdf}, abstract = {We present CPA-SymExec, a tool for symbolic execution that is implemented in the open-source, configurable verification framework CPAchecker. Our implementation automatically detects which symbolic facts to track, in order to obtain a small set of constraints that are necessary to decide reachability of a program area of interest. CPA-SymExec is based on abstraction and counterexample-guided abstraction refinement (CEGAR), and uses a constraint-interpolation approach to detect symbolic facts. We show that our implementation can better mitigate the path-explosion problem than symbolic execution without abstraction, by comparing the performance to the state-of-the-art Klee-based symbolic-execution engine Symbiotic and to Klee itself. For the experiments we use two kinds of analysis tasks: one for finding an executable path to a specific location of interest (e.g., if a test vector is desired to show that a certain behavior occurs), and one for confirming that no executable path to a specific location exists (e.g., if it is desired to show that a certain behavior never occurs). CPA-SymExec is released under the Apache 2 license and available (inclusive source code) at https://cpachecker.sosy-lab.org. A demonstration video is available at https://youtu.be/qoBHtvPKtnw.}, video = {https://youtu.be/7o7EtpbV8NM}, } -
Tests from Witnesses: Execution-Based Validation of Verification Results.
In 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
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)}, 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.}, } -
Reducer-Based Construction of Conditional Verifiers.
In Proceedings of the 40th International Conference on
Software Engineering (ICSE 2018, Gothenburg, Sweden, May 27 - June 3),
pages 1182-1193,
2018.
ACM.
doi:10.1145/3180155.3180259
Publisher's Version
PDF
Presentation
Supplement
Abstract
Despite recent advances, software verification remains challenging. To solve hard verification tasks, we need to leverage not just one but several different verifiers employing different technologies. To this end, we need to exchange information between verifiers. Conditional model checking was proposed as a solution to exactly this problem: The idea is to let the first verifier output a condition which describes the state space that it successfully verified and to instruct the second verifier to verify the yet unverified state space using this condition. However, most verifiers do not understand conditions as input. In this paper, we propose the usage of an off-the-shelf construction of a conditional verifier from a given traditional verifier and a reducer. The reducer takes as input the program to be verified and the condition, and outputs a residual program whose paths cover the unverified state space described by the condition. As a proof of concept, we designed and implemented one particular reducer and composed three conditional model checkers from the three best verifiers at SV-COMP 2017. We defined a set of claims and experimentally evaluated their validity. All experimental data and results are available for replication.BibTeX Entry
@inproceedings{ICSE18, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger and Heike Wehrheim}, title = {Reducer-Based Construction of Conditional Verifiers}, booktitle = {Proceedings of the 40th International Conference on Software Engineering (ICSE~2018, Gothenburg, Sweden, May 27 - June 3)}, pages = {1182-1193}, year = {2018}, publisher = {ACM}, doi = {10.1145/3180155.3180259}, sha256 = {}, url = {https://www.sosy-lab.org/research/reducer/}, pdf = {https://www.sosy-lab.org/research/pub/2018-ICSE.Reducer-Based_Construction_of_Conditional_Verifiers.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2018-06-01_ICSE18_ReducerBasedConstructionOfConditionalVerifiers_Marie.pdf}, abstract = {Despite recent advances, software verification remains challenging. To solve hard verification tasks, we need to leverage not just one but several different verifiers employing different technologies. To this end, we need to exchange information between verifiers. Conditional model checking was proposed as a solution to exactly this problem: The idea is to let the first verifier output a condition which describes the state space that it successfully verified and to instruct the second verifier to verify the yet unverified state space using this condition. However, most verifiers do not understand conditions as input. In this paper, we propose the usage of an off-the-shelf construction of a conditional verifier from a given traditional verifier and a reducer. The reducer takes as input the program to be verified and the condition, and outputs a residual program whose paths cover the unverified state space described by the condition. As a proof of concept, we designed and implemented one particular reducer and composed three conditional model checkers from the three best verifiers at SV-COMP 2017. We defined a set of claims and experimentally evaluated their validity. All experimental data and results are available for replication.}, } -
Abstraction Refinement for Model Checking: Program Slicing + CEGAR.
Master's Thesis, LMU Munich, Software Systems Lab,
2018.
PDF
BibTeX Entry
@misc{ThomasSlicing, author = {Thomas Lemberger}, title = {Abstraction Refinement for Model Checking: Program Slicing + {CEGAR}}, year = {2018}, pdf = {https://www.sosy-lab.org/research/msc/2018.Lemberger.Abstraction_Refinement_for_Model_Checking_Program_Slicing_and_Cegar.pdf}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
2017
-
Software Verification: Testing vs. Model Checking.
In Proceedings of the 13th Haifa Verification Conference (HVC 2017, Haifa, Israel, November 13-25),
LNCS 10629,
pages 99-114,
2017.
Springer.
doi:10.1007/978-3-319-70389-3_7
Publisher's Version
PDF
Presentation
Supplement
Abstract
In practice, software testing has been the established method for finding bugs in programs for a long time. But in the last 15 years, software model checking has received a lot of attention, and many successful tools for software model checking exist today. We believe it is time for a careful comparative evaluation of automatic software testing against automatic software model checking. We chose six existing tools for automatic test-case generation, namely AFL-fuzz, CPATiger, Crest-ppc, FShell, Klee, and PRtest, and four tools for software model checking, namely CBMC, CPA-Seq, ESBMC-incr, and ESBMC-kInd, for the task of finding specification violations in a large benchmark suite consisting of 5693 C programs. In order to perform such an evaluation, we have implemented a framework for test-based falsification (TBF) that executes and validates test cases produced by test-case generation tools in order to find errors in programs. The conclusion of our experiments is that software model checkers can (i) find a substantially larger number of bugs (ii) in less time, and (iii) require less adjustment to the input programs.BibTeX Entry
@inproceedings{HVC17, author = {Dirk Beyer and Thomas Lemberger}, title = {Software Verification: Testing vs. Model Checking}, booktitle = {Proceedings of the 13th Haifa Verification Conference (HVC~2017, Haifa, Israel, November 13-25)}, pages = {99-114}, year = {2017}, series = {LNCS~10629}, publisher = {Springer}, doi = {10.1007/978-3-319-70389-3_7}, sha256 = {}, url = {https://www.sosy-lab.org/research/test-study/}, pdf = {https://www.sosy-lab.org/research/pub/2017-HVC.Software_Verification_Testing_vs_Model_Checking.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2017-11-15_HVC17_TestStudy_Thomas.pdf}, abstract = {In practice, software testing has been the established method for finding bugs in programs for a long time. But in the last 15 years, software model checking has received a lot of attention, and many successful tools for software model checking exist today. We believe it is time for a careful comparative evaluation of automatic software testing against automatic software model checking. We chose six existing tools for automatic test-case generation, namely AFL-fuzz, CPATiger, Crest-ppc, FShell, Klee, and PRtest, and four tools for software model checking, namely CBMC, CPA-Seq, ESBMC-incr, and ESBMC-kInd, for the task of finding specification violations in a large benchmark suite consisting of 5693 C programs. In order to perform such an evaluation, we have implemented a framework for test-based falsification (TBF) that executes and validates test cases produced by test-case generation tools in order to find errors in programs. The conclusion of our experiments is that software model checkers can (i) find a substantially larger number of bugs (ii) in less time, and (iii) require less adjustment to the input programs.}, annote = {Won the HVC 2017 Best Paper Award}, }Additional Infos
Won the HVC 2017 Best Paper Award
2016
-
Symbolic Execution with CEGAR.
In 7th International Symposium on
Leveraging Applications of Formal Methods, Verification, and Validation
(ISoLA 2016, Part 1, Imperial, Corfu, Greece, October 10-14),
LNCS 9952,
pages 195-211,
2016.
Springer.
doi:10.1007/978-3-319-47166-2_14
Publisher's Version
PDF
Presentation
Supplement
Abstract
Symbolic execution, a standard technique in program analysis, is a particularly successful and popular component in systems for test-case generation. One of the open research problems is that the approach suffers from the path-explosion problem. We apply abstraction to symbolic execution, and refine the abstract model using counterexampleguided abstraction refinement (CEGAR), a standard technique from model checking. We also use refinement selection with existing and new heuristics to influence the behavior and further improve the performance of our refinement procedure. We implemented our new technique in the open-source software-verification framework CPAchecker. Our experimental results show that the implementation is highly competitive.BibTeX Entry
@inproceedings{ISOLA16a, author = {Dirk Beyer and Thomas Lemberger}, title = {Symbolic Execution with {CEGAR}}, booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2016, Part~1, Imperial, Corfu, Greece, October 10-14)}, pages = {195-211}, year = {2016}, series = {LNCS~9952}, publisher = {Springer}, doi = {10.1007/978-3-319-47166-2_14}, sha256 = {}, url = {https://www.sosy-lab.org/research/cpa-symexec/}, pdf = {https://www.sosy-lab.org/research/pub/2016-ISoLA.Symbolic_Execution_with_CEGAR.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2016-10-10_ISoLA16_SymbolicExecutionWithCegar_Dirk.pdf}, abstract = {Symbolic execution, a standard technique in program analysis, is a particularly successful and popular component in systems for test-case generation. One of the open research problems is that the approach suffers from the path-explosion problem. We apply abstraction to symbolic execution, and refine the abstract model using counterexampleguided abstraction refinement (CEGAR), a standard technique from model checking. We also use refinement selection with existing and new heuristics to influence the behavior and further improve the performance of our refinement procedure. We implemented our new technique in the open-source software-verification framework CPAchecker. Our experimental results show that the implementation is highly competitive.}, }
2015
-
Efficient Symbolic Execution using CEGAR over Two Abstract Domains.
Bachelor's Thesis, University of Passau, Software Systems Lab,
2015.
PDF
BibTeX Entry
@misc{ThomasSymbolicExecution, author = {Thomas Lemberger}, title = {Efficient Symbolic Execution using {CEGAR} over Two Abstract Domains}, year = {2015}, pdf = {https://www.sosy-lab.org/research/bsc/2015.Lemberger.Efficient_Symbolic_Execution_using_CEGAR_over_Two_Abstract_Domains.pdf}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }