Colloquium Loria – Jaco van de Pol

18 octobre 2021

Le prochain colloquium du Loria aura lieu le jeudi 28 octobre à 13h30 dans l’amphithéâtre du laboratoire.

Nous sommes ravis d’accueillir Jaco van de Pol, professeur d’informatique à Aarhus University. Il fera un exposé intitulé “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.