Automatically verified implementation of data structures based on AVL trees

Martin Clochard 1, 2
1 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 : We propose verified implementations of several data structures, including random-access lists and ordered maps. They are derived from a common parametric implementation of self-balancing binary trees in the style of Adelson-Velskii and Landis trees. The development of the specifications, mplementations and proofs is carried out using the Why3 environment. The originality of this approach is the genericity of the specifications and code combined with a high level of proof automation.
Type de document :
Communication dans un congrès
Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01067217
Contributeur : Claude Marché <>
Soumis le : mardi 23 septembre 2014 - 11:15:35
Dernière modification le : jeudi 9 février 2017 - 15:56:04
Document(s) archivé(s) le : mercredi 24 décembre 2014 - 20:53:16

Fichier

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

Identifiants

  • HAL Id : hal-01067217, version 1

Citation

Martin Clochard. Automatically verified implementation of data structures based on AVL trees. Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science. 〈hal-01067217〉

Partager

Métriques

Consultations de la notice

265

Téléchargements de fichiers

153