Abstract
In this first seminar of the year, we discussed the mechanized implementation of program logic for software written in the C language using Frama-C/WP.
Loïc Correnson discussed the difficulty of mastering the complexity of the weakest precondition calculus - weakest precondition calculus or " wp " - and the importance of the memory model and simplifying proof obligations. From the user's point of view, he presented the main methodological approaches for industrially tackling the proof of complex programs.
Finally, he posed the question of the " quality " of a proof and its basis of trust, which finally enabled him to revisit the test & proof duality in a surprising way.
