Causality and Responsibility for Formal Verification and Beyond
It addresses the need for intuitive explanations and improved metrics in formal verification, with incremental extensions to existing causality theory.
The paper explores applications of actual causality theory and degree of responsibility to formal verification, including explaining counterexamples, refining coverage metrics, and symbolic trajectory evaluation, and briefly mentions recent uses in legal reasoning.
The theory of actual causality, defined by Halpern and Pearl, and its quantitative measure - the degree of responsibility - was shown to be extremely useful in various areas of computer science due to a good match between the results it produces and our intuition. In this paper, I describe the applications of causality to formal verification, namely, explanation of counterexamples, refinement of coverage metrics, and symbolic trajectory evaluation. I also briefly discuss recent applications of causality to legal reasoning.