Abstraction in Model Checking for Bug Hunting

Temporal logic model checking is one of the most widely used verification techniques. It allows to automatically decide if a design satisfies its specification. When the specification does not hold an explanation of the offending behavior is produced. Even if it has been proved to be effective in practice this technique suffers of the state explosion problem. To tackle this problem various techniques have been proposed. One of the most promising and used is abstraction. An abstraction of the design is computed and the standard model checking algorithms are applied on this abstraction. If the property is verified in the abstract model, then the property is verified in the original design too. Vice versa does not usually hold. The aim of this work is in extending the work done in abstraction and model checking using abstraction in buggy design, thus refining the counterexamples/witnesses of a given temporal property to make it possible to correct the design