Guest Talk: Christel Baier: From verification to causality-based explications

Tuesday, May 17, 2022, 11:00am

Location: Department of Computer Science - Ahornstr. 55, building E3, 2nd floor, room 9222
and online:
Link: https://rwth.zoom.us/my/moves
Meeting ID: 215 989 3416

Speaker: Christel Baier

 

Abstract: 

The early success story of the model checking approach relies fundamentally on two features. First, the algorithms provide a push-button technology: As soon as the model and specification have been generated, one obtains a result in a fully automated way. Second, if the algorithm terminates with a negative result, then it can infer counterexamples to the specification. Counterexamples are the first instances for what we use the term explication, which refers to a mathematical concept that in some way sheds light on why the model checker has returned the result. While counterexamples are single instances of execution traces violating the specification, they provide little insights in what causes the specification violation. To enhance the system transparency, more crisp explications for the satisfaction or violation of properties are demanded. The talk presents an overview of techniques that go in this direction by using formal notions of causality and responsibility to explicate verification results.