Verified Analysis of Functional Data Structures

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

Abstract

In recent work the author has analyzed a number of classical functional search tree and priority queue implementations with the help of the theorem prover Isabelle/HOL. The functional correctness proofs of AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2 brother trees, AA trees and splay trees could be automated. The amortized logarithmic complexity of skew heaps, splay trees, splay heaps and pairing heaps had to be proved manually.

Original languageEnglish
Title of host publication1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
EditorsDelia Kesner, Brigitte Pientka
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770101
DOIs
StatePublished - 1 Jun 2016
Event1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal
Duration: 22 Jun 201626 Jun 2016

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume52
ISSN (Print)1868-8969

Conference

Conference1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
Country/TerritoryPortugal
CityPorto
Period22/06/1626/06/16

Keywords

  • Algorithm Analysis
  • Functional Programming
  • Program Verification

Fingerprint

Dive into the research topics of 'Verified Analysis of Functional Data Structures'. Together they form a unique fingerprint.

Cite this