Compositional safety refutation techniques

Kumar, Madhukar, Schrammel, Peter and Mandayam, Srivas (2017) Compositional safety refutation techniques. 15th International Symposium on Automated Technology for Verification and Analysis, Pune, India, 3-6 October 2017. Published in: Automated Technology for Verification and Analysis. 164-183. Springer ISBN 9783319681665

[img] PDF (The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-68167-2_12) - Accepted Version
Download (278kB)

Abstract

One 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.

Item Type: Conference Proceedings
Keywords: verification, refutation, inter-procedural analysis, backwards analysis
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Q Science > QA Mathematics > QA0076 Computer software
Depositing User: Peter Schrammel
Date Deposited: 02 Aug 2017 09:28
Last Modified: 19 Oct 2017 12:54
URI: http://sro.sussex.ac.uk/id/eprint/69533

View download statistics for this item

📧 Request an update