BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Model Checking: Around verification: Explaining specifications and
  outputs of the model checker. - Hana Chockler (King's College London)
DTSTART:20220722T110000Z
DTEND:20220722T114500Z
UID:TALK176741@talks.cam.ac.uk
DESCRIPTION:In this talk I will focus on the interaction with the model-ch
 ecking tool: writing specifications and understanding the model checker's 
 output. I will argue that tools like learning and causality can help with 
 both tasks and reduce the amount of human effort required for verification
 . I will further discuss how explanations can help us to understand the mo
 del. I will briefly touch on the theory of actual causality and illustrate
  the definitions by examples from formal verification. I will also argue t
 hat active learning can be viewed as a type of causal discovery.&nbsp\;\nB
 io: Hana Chockler is a Principal Scientist at a startup company causaLens 
 and a Reader (Associate Professor) in Formal Methods in the Department of 
 Informatics at King&rsquo\;s College London (KCL). Prior to joining KCL in
  2013\, Hana worked at IBM Research in the formal verification and softwar
 e engineering departments. Her research interests span a wide variety of t
 opics\, including formal verification and synthesis of hardware and softwa
 re\, fundamental concepts in causality and its applications to a variety o
 f domains\, learning\, and explainable AI.\n&nbsp\;
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR