Handcrafted Inversions Made Operational on Operational Semantics

Jean-François Monin 1, 2 Xiaomu Shi 1
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : When reasoning on formulas involving large-size inductively defined relations, such as the semantics of a real programming language, many steps require the inversion of a hypothesis. The built-in "inversion" tactic of Coq can then be used, but it suffers from severe controllability, maintenance and efficiency issues, which makes it unusable in practice in large applications. To circumvent this issue, we propose a proof technique based on the combination of an antidiagonal argument and the impredicative encoding of inductive data-structures. We can then encode suitable helper tactics in LTac, yielding scripts which are much shorter (as well as corresponding proof terms) and, more importantly, much more robust against changes in version changes in the background software. This is illustrated on correctness proofs of non-trivial C programs according to the operational semantics of C defined in CompCert
keyword : Coq inversion
Type de document :
Communication dans un congrès
Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. ITP 2013 - 4th International Conference Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.338-353, 2013, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_25〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00937168
Contributeur : Jean-François Monin <>
Soumis le : lundi 27 janvier 2014 - 23:18:37
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : lundi 28 avril 2014 - 01:50:09

Fichier

itp13.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Jean-François Monin, Xiaomu Shi. Handcrafted Inversions Made Operational on Operational Semantics. Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. ITP 2013 - 4th International Conference Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.338-353, 2013, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_25〉. 〈hal-00937168〉

Partager

Métriques

Consultations de la notice

413

Téléchargements de fichiers

117