A Certified Procedure for RL Verification

Abstract : Proving programs correct is hard. During the last decades computer scientists developed various logics dedicated to program verification. One such effort is Reachability Logic (RL): 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 (i.e., an insufficient assumption, implicit hypotheses, and a missing case in the paper proof). The Coq formalisation provides us with a certified program-verification procedure.
Type de document :
Communication dans un congrès
SYNASC 2017 : 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timisoara, Romania. pp.8, 2017, IEEE CPS (to appear)
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01627517
Contributeur : Pal Dream <>
Soumis le : mercredi 1 novembre 2017 - 21:25:16
Dernière modification le : mardi 3 juillet 2018 - 11:34:59
Document(s) archivé(s) le : vendredi 2 février 2018 - 12:55:51

Fichier

synasc2017.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01627517, version 1

Collections

Citation

Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu. A Certified Procedure for RL Verification. SYNASC 2017 : 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timisoara, Romania. pp.8, 2017, IEEE CPS (to appear). 〈hal-01627517〉

Partager

Métriques

Consultations de la notice

169

Téléchargements de fichiers

123