Skip to Main content Skip to Navigation
Conference papers

Automatically verified implementation of data structures based on AVL trees

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-01067217
Contributor : Claude Marché <>
Submitted on : Tuesday, September 23, 2014 - 11:15:35 AM
Last modification on : Wednesday, September 16, 2020 - 5:23:03 PM
Long-term archiving on: : Wednesday, December 24, 2014 - 8:53:16 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01067217, version 1

Collections

Citation

Martin Clochard. Automatically verified implementation of data structures based on AVL trees. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. ⟨hal-01067217⟩

Share

Metrics

Record views

718

Files downloads

675