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

https://hal.inria.fr/hal-00937168
Contributor : Jean-François Monin <>
Submitted on : Monday, January 27, 2014 - 11:18:37 PM
Last modification on : Friday, November 6, 2020 - 4:09:05 AM
Long-term archiving on: : Monday, April 28, 2014 - 1:50:09 AM

File

itp13.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

673

Files downloads

489