Home | Legals | Sitemap | KIT

Feature Enrichment of InspectJ

Feature Enrichment of InspectJ
time:As soon as possible
contact person:

Mana Taghdiri, Tianhai Liu

InspectJ is a bounded program verification tool developed in Automated Software Analysis group. Given Java programs annotated with JML, InspectJ tries to find counterexamples in a bounded scope. Parts of Java and JML features have been already supported in the current version of InspectJ, e.g.:

  • Java types: integer, boolean, array, class
  • Method call
  • Class inheritance
  • Object casting
  • Java operators
  • Java structured loops
  • JML features from level 0 plus \reach

The task is to design and implement other necessary features of Java and JML, e.g:

  • Abstract class and Interface
  • Java exception handling
  • Java unstructed loops
  • Java static members
  • JML loop invariant
  • JML exception behavior
  • JML model ObjectSet


  • Familiarity with first order logic.
  • Experience in Java is necessary.
  • Knowledge in JML is helpful.


If interested, please contact mana.taghdiri@kit.edu or tianhai.liu@kit.edu