Sites Inria

English version

Séminaires des équipes de recherche

Reflecting Modular Automation

Séminaire Gallium - Moscova

  • Date : 18/01/2013
  • Lieu : Inria - Rocquencourt - Amphithéâtre Alan Turing
  • Intervenant(s) : Gregory Malecha - Harvard University
  • Organisateur(s) : Gallium - Moscova

I describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional methods which rely on run-time generation and checking of proofs, we use verified-correct procedures with Coq soundness proofs. Though they are internalized in Coq's logic, our provers support user extensions to enable reasoning over new domains and about abstract predicates. These extensions can be modularly combined into reusable "strategies" that can be applied in many contexts. This is
enabled by a rich handling of unification and a formulation of environments that supports extension. We instantiate the technique to the verification of imperative programs and show how reflective tactics can be used to reduce heap implications contains abstract predicates.

Mots-clés : Paris - Rocquencourt Séminaire Moscova Gallium

Haut de page

Suivez Inria