Computing Specification-Sensitive Abstractions for Program Verification
Tianhai Liu, Shmuel S. Tyszberowicz, Mihai Herda, Bernhard Beckert,
Daniel Grahl, and Mana Taghdiri
To enable scalability and address the needs of real-world software, deductive
verification relies on modularization of the target program and decomposition
of its requirement specification. In this paper, we present an approach that,
given a Java program and a partial requirement specification written using the
Java Modeling Language, constructs a semantic slice. In the slice, the parts
of the program irrelevant w.r.t. the partial requirements are replaced by an
abstraction. The core idea of our approach is to use bounded program
verification techniques to guide the construction of these slices. Our
approach not only lessens the burden of writing auxiliary specifications (such
as loop invariants) but also reduces the number of proof steps needed for
verification.