Why does it fail? Explanation of verification failures

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.

Figures (3)

• Figure 1: Railway system
• Figure 2: Explanation tree
• Figure 3: Alternative explanation tree

Theorems & Definitions (5)

• definition 1: $\mathit{expl}$ and $\mathit{intr}$
• definition 2: $\mathit{rewrite}$
• definition 3: $\mathcal{L}$-alternate
• definition 4: Provenance
• definition 5: $\mathcal{Y}$