Title | Bounded verification with on-the-fly discrepancy computation |
Publication Type | Conference Paper |
Year of Publication | 2015 |
Authors | Fan C, Mitra S |
Conference Name | Automated Technology for Verification and Analysis - 13th International Symposium, (ATVA) |
Date Published | oct |
Publisher | Springer, Cham |
Conference Location | Shanghai, China |
ISBN Number | 9783319249520 |
Abstract | Existing program analysis tools that implement abstraction rely on saturating procedures to compute over-approximations of$\backslash$n fixpoints. As an alternative, we propose a new algorithm to compute an over-approximation of the set of reachable states of$\backslash$n a program by replacing loops in the control flow graph by their abstract transformer. Our technique is able to generate diagnostic$\backslash$n information in case of property violations, which we call leaping counterexamples. We have implemented this technique and report experimental results on a set of large ANSI-C programs using abstract domains$\backslash$n that focus on properties related to string-buffers. |
URL | http://link.springer.com/10.1007/978-3-319-24953-7{\_}32 |
DOI | 10.1007/978-3-319-24953-7_32 |
Bounded verification with on-the-fly discrepancy computation
Submitted by chuchu@mit.edu on