Séminaires des équipes de recherche
Reflecting Modular Automation
- 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.