Abstract:

An interpolation based method was proposed to automatically understand counterexamples produced by model checker. By this method the we
akest precondition of a counterexample was first derived from its failure state, and then inconsistent analysis was performed on the initial state and the weakest precondition of the counterexample. Craig interpolations which can be extracted in linear time are the causes of model failure; these causes can be mapped to corresponding events directly. Experimental results show that our method improves the efficiency of understanding counterexamples remarkably, which can reduce the burden of software debugging workers and promote reliability and quality imp
rovement of software.

Key words:  model checking, counterexample, understanding counterexample, weakest precondition, Craig interpolation