Formal Proof of Soundness for an RL Prover

Abstract : Proving programs correct is one of the major challenges that computer scientists have been struggling with during the last decades. For this purpose, Reachability Logic (RL) was proposed as a language-parametric generalisation of Hoare Logic. Recently, based on RL, an automatic verification procedure was given and proved sound. In this paper we generalise this procedure and prove its soundness formally in the Coq proof assistant. For the formalisation we had to deal with all the minutiae that were neglected in the paper proof. The trickiest one was appropriate renaming of free variables which, we discovered, was handled in the paper proof using an insufficient assumption. We also discovered a missing case in the paper proof, and we clarified some implicit and hidden hypotheses. Last but not least, the Coq formalisation provides us with a certified program-verification procedure.
Type de document :
Rapport
[Research Report] RR-471, INRIA Lille - Nord Europe; Alexandru Ioan Cuza, University of Iasi. 2015, pp.27
Liste complète des métadonnées

https://hal.inria.fr/hal-01244578
Contributeur : Pal Dream <>
Soumis le : mardi 15 décembre 2015 - 23:50:13
Dernière modification le : vendredi 16 septembre 2016 - 15:16:52
Document(s) archivé(s) le : samedi 29 avril 2017 - 15:58:52

Fichier

RR-471.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01244578, version 1

Citation

Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu. Formal Proof of Soundness for an RL Prover. [Research Report] RR-471, INRIA Lille - Nord Europe; Alexandru Ioan Cuza, University of Iasi. 2015, pp.27. <hal-01244578>

Partager

Métriques

Consultations de
la notice

363

Téléchargements du document

192