Producing All Ideals of a Forest, Formally (Verification Pearl)

Jean-Christophe Filliâtre 1, 2 Mário Pereira 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : In this paper we present the first formal proof of an implementation of Koda and Ruskey's algorithm, an algorithm for generating all ideals of a forest poset as a Gray code. One contribution of this work is to exhibit the invariants of this algorithm, which proved to be challenging. We implemented, specified, and proved this algorithm using the Why3 tool. This allowed us to employ a combination of several automated theorem provers to discharge most of the verification conditions, and the Coq proof assistant for the remaining two.
Type de document :
Communication dans un congrès
VSTTE 2016, Jul 2016, Toronto, Canada. pp.46 - 55, 2016, 〈10.1007/978-3-319-48869-1_4〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01316859
Contributeur : Mário José Parreira Pereira <>
Soumis le : mardi 29 novembre 2016 - 14:21:58
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : lundi 27 mars 2017 - 08:32:12

Fichier

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

Identifiants

Citation

Jean-Christophe Filliâtre, Mário Pereira. Producing All Ideals of a Forest, Formally (Verification Pearl). VSTTE 2016, Jul 2016, Toronto, Canada. pp.46 - 55, 2016, 〈10.1007/978-3-319-48869-1_4〉. 〈hal-01316859v2〉

Partager

Métriques

Consultations de la notice

204

Téléchargements de fichiers

47