To enable scalability and address the needs of real-world software, deductive verification relies on decomposition and modularization of the target program and 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 (JML), 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 program annotations (such as loop invariants) but also reduces the number of proof steps needed for verification.
- Computing Specification-Sensitive Abstractions for Program Verification, Tianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, and Mana Taghdiri, 2th Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA), November, 2016
- Tianhai Liu
- Mihai Herda
- Shmuel Tyszberowicz
- Daniel Grahl
- Mana Taghdiri
- Bernhard Beckert
- AbstractJ: AbstractJ.jar, It is compiled in OpenJDK 1.7.
- Third-party software: ext-lib.zip. It consists of some libraries obtained from Z3, Soot, Guava, Jung, Jacoco and Apache Collections.
- Solver: Z3JNI.zip. It contains two Z3 compiled library files for 64-bit Linux. For additional platform supports, please compile Z3 following the instructions from Leonardo de Moura.
- KeY binary: KeY.zip. KeY with the option to disable checking runtime exceptions. Requires Java1.7 and Linux. Run it by
tpyingthe following commands in a terminal: java -jar KeY.jar. After loading a program, you need change the runtime-exceptionoption to slicing in the menu: Options-> TacletOptions -> runtimeExceptions. After it is set to slicing, you have to restart KeY.
- All experiments can be found here: experiments.zip.