Sites Inria

Version française

Séminaire des équipes de recherche

Verified Characteristic Formulae for CakeML

© INRIA Sophie Auvin - G comme Grille

  • Date : 18/04/2017
  • Place : 2 rue Simone Iff (ou: 41 rue du Charolais) - Salle Lions 1, bâtiment C - 10h30
  • Guest(s) : Armaël Guéneau

Characteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered with respect to an informal specification of a programming language (OCaml).

In this talk, I will explain how we built a fully-fledged CF framework for the formally specified CakeML programming language. Our framework extends the existing CF approach to support exceptions and I/O, thereby covering the full feature set of CakeML, and comes with a formally verified soundness theorem. I will also show how the CF framework integrates with existing proof techniques for verifying CakeML programs. This validates the CF approach, and allows users to prove end-to-end theorems for higher-order imperative programs.

Keywords: Gallium Inria de Paris Characteristic Formulae CakeML