Approximating the Safely Reusable Set of Learned Facts
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@article{bh09approximating,
author = {Domagoj Babi\'c and Alan J.~Hu},
title = {{Approximating the Safely Reusable Set of Learned Facts}},
journal = {STTT: International Journal on Software Tools for
Technology Transfer},
volume = {11},
number = {4},
year = {2009},
pages = {325--338},
publisher = {Springer},
}
Abstract:
Despite many advances, today's software model checkers and extended static
checkers still do not scale well to large code bases, when verifying properties
that depend on complex interprocedural flow of data. An obvious approach to
improve performance is to exploit software structure. Although a tremendous
amount of work has been done on exploiting structure at various levels of
granularity, the fine-grained shared structure among multiple verification
conditions has been largely ignored. In this paper, we formalize the notion of
shared structure among verification conditions, and propose a novel and
efficient approach to exploit this sharing by safely reusing facts learned while
checking one verification condition to help solve the others. Experimental
results show that this approach can improve the performance of verification,
even on path- and context-sensitive and dataflow-intensive properties.