Computing Specification-Sensitive Abstractions for Program Verification
-
Author:
Tianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl and Mana Taghdiri
-
Place:
2th Symposium on Dependable Software Engineering Theories, Tools and Applications
- Date: November 2016
-
Abstract
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.
BibTex
@InProceedings{abstractj,
author = {Tianhai Liu and Shmuel Tyszberowicz and Mihai Herda and Bernhard Beckert and Daniel Grahl and Mana Taghdiri},
title = {Computing Specification-Sensitive Abstractions for Program Verification},
booktitle = {2th Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA)},
year = {2016},
month = {November}
}