InspectJ: Bounded Verification Tool for Java

InspectJ is a bounded program verification tool for Java programs annotated with Java Modeling Language (JML) -- a behavioral specification language which integrates almost seamlessly into Java. Given a Java method and its specification, i.e. class invariants, and/or pre- and post-conditions, InspectJ will automatically produce logical formulas in a first-order SMT-LIB theory that includes  bit-vectors and arrays. The formulas will be handled by a satisfiability engine -- currently Z3 -- for a solution. A solution represents  a voilation of the specification. In addition to that, InspectJ also finds runtime exceptions such as ArrayIndexOutOfBound and NullPointerDereferencing.

InspectJ is incomplete, because it analyzes only a bounded scope in which the number of instances of each class, the number of loop (and recursive call) iterations, and the bitwidth of integers are bounded by the user. Although the analysis is sound, which means that the bugs it finds are feasible in the original code (with respect to the analyzed scope), it cannot make any guarantees beyond the scope.

publications

• Bounded Program Verification using an SMT Solver: A Case Study, Tianhai Liu, Michael Nagel, Mana Taghdiri, 5th International Conference on Software Testing, Verification and Validation (ICST), April, 2012.

   

People

• Mana Taghdiri
• Tianhai Liu
• Michael Nagel
• Mihai Herda

Tool

If you are interested in the InspectJ, please contact Tianhai Liu or Mana Taghdiri.