Technical Report No. 180 - Abstract

Tilman Mehler, Stefan Edelkamp
Trail-directed Java Program Verification

This paper introduces the application of trail-based heuristics for software verification. Trail-directed program verification serves the purpose of shortening an error trail, so that it will be more comprehensible for the user. We explain the concept of two heuristics that are based on the Hamming- and FSM-distance between states of a Java program. We then utilize the Java software verifier JPF to implement and test the new heuristics and to compare them to the heuristics that are already provided by this tool.