Exploiting Shared Structure in Software Verification Conditions
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{bh07sharing,
author = {Domagoj Babi\'c and Alan J. Hu},
title = {{Exploiting Shared Structure in Software Verification Conditions}},
editor = {Karen Yorav},
booktitle = {HVC'07: Proceedings of Haifa Verification Conference},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4899},
pages = {169--184},
year = {2007},
location = {Haifa, Israel},
}
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, propose a novel and efficient
approach to exploit this sharing, and provide experimental results that this approach
can significantly improve the performance of verification, even on pathand
context-sensitive and dataflow-intensive properties.