paper.pdf (272.15 kB)
Compositional safety refutation techniques
conference contribution
posted on 2023-06-09, 07:30 authored by Madhukar Kumar, Peter Schrammel, Srivas MandayamOne of the most successful techniques for refuting safety properties is to find counterexamples by bounded model checking. However, for large programs, bounded model checking instances often exceed the limits of resources available. Generating such counterexamples in a modular way could speed up refutation, but it is challenging because of the inherently non-compositional nature of these counterexamples. We start from the monolithic safety verification problem and present a step-by-step derivation of the compositional safety refutation problem. We give three algorithms that solve this problem, discuss their properties with respect to efficiency and completeness, and evaluate them experimentally.
History
Publication status
- Published
File Version
- Accepted version
Journal
Automated Technology for Verification and AnalysisPublisher
SpringerPublisher URL
Page range
164-183Event name
15th International Symposium on Automated Technology for Verification and AnalysisEvent location
Pune, IndiaEvent type
conferenceEvent date
3-6 October 2017ISBN
9783319681665Series
Lecture notes in computer scienceDepartment affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2017-08-02First Open Access (FOA) Date
2017-10-13First Compliant Deposit (FCD) Date
2017-08-01Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC