Online / 6 & 7 February 2021

visit

Claire Dross

Claire Dross has a PhD in deductive verification of programs using a satisfiability modulo theory solver with the Université Paris-Sud (France). She has been working at AdaCore for the last 10 years on the development of the SPARK open-source tool for formal verification of the Ada language.

Events

Title Day Room Track Start End
Proving heap-manipulating programs with SPARK
The SPARK open-source proof tool for Ada now supports verifying pointer-based algorithms thanks to an ownership policy inspired by Rust		 Saturday D.safety Safety and Open Source 13:30 14:30