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

 Requirements:

• 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