Home // VALID 2013, The Fifth International Conference on Advances in System Testing and Validation Lifecycle // View article

Efficient Elimination of False Positives Using Bounded Model Checking

Authors:
Tukaram Muske
Advaita Datar
Mayur Khanzode
Kumar Madhukar

Keywords: Abstract Interpretation; Model Checking; False Positives Elimination, Data Flow Analysis

Abstract:
Software verification using abstract interpretation is scalable but imprecise. Model checking is precise in verifying a property but not scalable. Often, these two techniques are combined to achieve better precision. A possible way is to analyze a software system first by using abstract interpretation and later eliminating the false positives using bounded model checking. This is a time consuming process as it typically involves verifying an assertion corresponding to each generated warning. We observe verifying all assertions often introduces redundancy, and some verifications may not even eliminate a false positive. In this paper, we present an approach consisting of three techniques to make such false positives elimination faster. Two of the techniques identify an assertion as being equivalent to an other assertion thus avoiding its verification. The third technique tries to identify and skip a class of assertion verifications that will not eliminate a false positive. Empirical results indicate that these techniques are quite useful in reducing the number of assertions being verified by 53%, and the false positives elimination time by 60%.

Pages: 13 to 20

Copyright: Copyright (c) IARIA, 2013

Publication date: October 27, 2013

Published in: conference

ISSN: 2308-4316

ISBN: 978-1-61208-307-0

Location: Venice, Italy

Dates: from October 27, 2013 to October 31, 2013