Automated Software Analysis Group
Automated Software Analysis Group
Automated Software Analysis Group
Startseite
Research
AbstractJ

Computing Specification-Sensitive Abstractions for Program Verification

To enable scalability and address the needs of real-world software, deductive veri fication relies on decomposition and modularization of the target program and its requirement speci fication. In this paper, we present an approach that, given a Java program and a partial requirement specifi cation 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 verifi cation 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 verifi cation.

 

Publications

People

  • Tianhai Liu
  • Mihai Herda
  • Shmuel Tyszberowicz
  • Daniel Grahl
  • Mana Taghdiri
  • Bernhard Beckert

Tools

  • 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 tpying the following commands in a terminal: java -jar KeY.jar. After loading a program, you need change the runtime-exception option to slicing in the menu: Options-> Taclet Options -> runtimeExceptions. After it is set to slicing, you have to restart KeY.

  

 Experiments