WG211/M19Lawall
From WG 2.11
Julia's adventures with Why3
Why3 is a platform for deductive program verification developed in the Inria Toccata team. In the Inria Whisper team, we have been exploring the use of domain-specific languages to develop formally verified operating system components. This talk will present our exploration of the use of Why in the verification of multicore process schedulers, developed using the DSL Ipanema.
Joint work with Gilles Muller, Virginia Aponte, and the rest of the Ipanema team.
