Vérification de programmes OCaml fortement impératifs avec Why3

Conference object French OPEN
Filliâtre, Jean-Christophe; Pereira, Mário; Melo De Sousa, Simão;
(2018)
  • Publisher: HAL CCSD
  • Subject: [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

International audience; Cet article présente une méthodologie pour prouver des programmes OCaml fortement impératifs avec l'outil de vérification déductive Why3. Pour un programme OCaml donné, un modèle mémoire spécifique est construit et on vérifie un programme Why3 qu... View more
Share - Bookmark