Jaco van de Pol : Explainable Verification of Safety and Security of Software Systems

Verification of safety-critical (software) systems is essential, but requires automation to be applied full scale. The first half of the presentation will mention contributions that pushed the scalability of verification, in particular symbolic and parallel algorithms that are applied in model checkers.

However, fully automated verification poses new challenges. Certification: why can we trust the yes/no answer of a complicated tool like an automated model checker? Explainability: which result has actually been demonstrated, and under what assumptions?

Finally, I will introduce the notion of certified model checking, and illustrate it on a concrete approach for verification based on timed automata.