Why does it fail? Explanation of verification failures

TL;DR

This paper introduces a method to explain verification failures in formal methods by translating counterexamples into application domain terms, aiding practitioners in fault diagnosis.

Contribution

It presents a novel approach that uses predicate relevance and dependencies to generate understandable explanations of verification failures.

Findings

Effective in identifying relevant predicates in failure explanations

Improves understanding of complex counterexamples

Demonstrated on real verification examples

Abstract

Satisfiability solving is a common technique for formal verification forming the basis of many proof and model checking systems. Failure to show a proof obligation will produce a counterexample or failure trace with typically many thousands or even millions of boolean variables. Interpreting such a counterexample poses a challenge. Even if the individual variables are all understood, it is difficult to form a "big picture" of the situation causing the failure. We consider the case where verification conditions are expressed using concepts from a formal application domain model in a language based on predicate logic or a similar language. We introduce a method to explain verification failures in application domain terms. A measure of the relative relevance of predicates is used to extract the parts of a formula most likely to contribute meaningfully to the explanation. Dependencies between predicates are used to form a branching sequence of successive explanations. These explanations can help a practitioner find faults in the system being verified. The method is demonstrated on examples and compared to other methods.