Difference between revisions of "WG211/M19Lawall"
From WG 2.11
(Created page with "Julia's adventures with Why3 [http://why3.lri.fr/ Why3] is a platform for deductive program verification developed in the Inria Toccata team. In the Inria Whisper team, we h...") |
|||
Line 2: | Line 2: | ||
[http://why3.lri.fr/ 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. | [http://why3.lri.fr/ 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. |
Latest revision as of 21:20, 26 April 2019
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.