Un mécanisme d'extraction vers C pour Why3

National audienceNous présentons un mécanisme d'extraction d'un sous-ensemble des programmes écrits avec l'outil de vérification Why3 vers le langage C. Un modèle mémoire partiel mais simple permet aux utilisateurs d'écrire des programmes Why3 dans un style impératif très proche du C, avec une gestion manuelle et vérifiée formellement de la mémoire. De tels programmes peuvent ensuite être extraits de manière transparente vers du code C idiomatique, ce qui évite d'introduire des pertes de performances à l'extraction