Compositional safety refutation techniques

Kumar, Madhukar, Schrammel, Peter and Mandayam, Srivas (2017) Compositional safety refutation techniques. Published in: Automated Technology for Verification and Analysis. Springer (Accepted)

[img] PDF - Accepted Version
Restricted to SRO admin only

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: 02 Aug 2017 09:28
URI: http://sro.sussex.ac.uk/id/eprint/69533

View download statistics for this item

📧 Request an update