The Faculty of Informatics is pleased to announce a seminar given by Hana Chocker
TITLE: Causality and Formal Verification
SPEAKER: Hana Chocker, Research Staff Member at IBM Research Labs in Haifa, Israel
DATE: Wednesday, March 18th, 2009
PLACE: USI Università della Svizzera italiana, room SI-013, Informatics building (Via G. Buffi 13)
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. Formal verification is the mathematical method of checking the correctness of computerized systems by automatically proving their correctness with respect to a specification expressed in some formal way (for example, as a temporal logic formula). 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.
The talk does not require any prior knowledge of the research areas mentioned above.
Hana Chockler is a Research Staff Member at IBM Research Labs in Haifa, Israel. She has been at IBM since 2005. She was previously a visiting scientist at the Massachusetts Institute of Technology, and she did postdoctoral work at Worcester Polytechnic Institute and Northeastern University. Hana has a Ph.D. in computer science from the Hebrew University of Jerusalem. Her interests span formal and informal verification methods, as well as verification of hardware and embedded software.
HOST: Prof. Natasha Sharygina