skip to content

Causality and Responsibility in Formal Verification and Beyond

Presented by: 
Hana Chockler
Tuesday 27th September 2016 - 14:15 to 15:00
INI Seminar Room 1
In this talk, I will (briefly) introduce the theory of actual causality as defined by Halpern and Pearl. This theory turns out to be extremely useful in various areas of computer science (and also, perhaps surprisingly, psychology) due to a good match between the results it produces and our intuition. I will outline the evolution of the definitions of actual causality and intuitive reasons for the many parameters in the definition using examples from formal verification. I will also introduce the definitions of responsibility and blame, which quantify the definition of causality.

We will look in more detail at the applications of causality to formal verification, namely, explanation of counter-examples, refinement of coverage metrics, and symbolic trajectory evaluation. It is interesting to note that explanation of counter-examples using the definition of actual causality is implemented in an industrial tool and produces results that are usually consistent with the users’ intuition, hence it is a popular and widely used feature of the tool.

Finally, I will briefly discuss recent applications of causality to legal reasoning and to understanding of political phenomena, and will conclude with outlining promising future directions.

The talk is based on many papers written by many people, and is not limited to my own research. The talk is reasonably self-contained.
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons