Causality and Formal Verification

Hana Chockler (IBM Research)

Info

Date	20th March 2009 (week 9, Hilary Term 2009)
Time	15:00
Place	Room 441

Abstract

The formal definition of causality by Halpern and Pearl extends straightforward counterfactual causality. Causality and its quantitative measure responsibility allow us to compute causes for events and the exact responsibility of each cause for the event. As we will see in several examples, Halpern and Pearl's definition matches our intuition about what should be considered a cause. It also unexpectedly comes in handy in formal verification. Many areas in formal verification, such as coverage estimation, vacuity detection, symbolic trajectory evaluation (STE), and counterexamples explanation can be viewed in the framework of causality. Moreover, in these areas, causality and responsibility give additional insights into the problem and allow us to produce more accurate solutions.

The talk is based on joint work with J.Y. Halpern, O. Kupferman, O. Strichman, A. Yadgar, O. Grumberg, I. Beer, S. Ben-David, A. Orni, and R. Trefler.