Next Colloquium Loria will take place on Thursday, 28 October at 1:30 pm in the Amphitheater.
We are delighted to welcome Jaco van de Pol, Professor of Computer Science in Aarhus University, with a talk entitled “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.
