Skip to Main content Skip to Navigation
Conference papers

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
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Jean-François Monin Connect in order to contact the contributor
Submitted on : Monday, January 27, 2014 - 11:18:37 PM
Last modification on : Thursday, February 3, 2022 - 11:16:03 AM
Long-term archiving on: : Monday, April 28, 2014 - 1:50:09 AM


Publisher files allowed on an open archive




Jean-François Monin, Xiaomu Shi. Handcrafted Inversions Made Operational on Operational Semantics. ITP 2013 - 4th International Conference Interactive Theorem Proving, Jul 2013, Rennes, France. pp.338-353, ⟨10.1007/978-3-642-39634-2_25⟩. ⟨hal-00937168⟩



Record views


Files downloads