User: Guest  Login
Document type:
Bachelorarbeit 
Author(s):
Mündler, Niels 
Title:
A Verified Imperative Implementation of B-Trees 
Translated title:
Eine Verifizierte Imperative Implementierung von B-Bäumen 
Abstract:
In this thesis, we use the interactive theorem prover Isabelle/HOL to verify an imperative implementation of the classical B-tree data structure. The implementation supports set membership and insertion queries with efficient binary search for intra-node navigation. This is accomplished by first specifying the structure abstractly in the functional modeling language HOL and proving functional correctness. Using manual refinement, we derive an imperative implementation in Imperative/HOL....    »
 
Translated abstract:
In dieser Arbeit wird mithilfe des interaktiven Theorembeweisers Isabelle/HOL eine imperative Version der klassischen B-Baum Datenstruktur verifiziert. Die Implementierung unterstützt Element- und Einfügeoperationen mit effizienter binärerer Suche für knoteninterne Navigation. Das Ergebnis wurde erzielt, indem die Struktur zuerst abstrakt in der Modellierungssprache HOL spezifiziert wurde, in der funktionale Korrektheit gezeigt werden konnte. Mithilfe von Verfeinerung wurde davon eine imperati...    »
 
Subject:
DAT Datenverarbeitung, Informatik 
DDC:
000 Informatik, Wissen, Systeme 
Advisor:
Nipkow, Tobias (Prof. Dr.); Lammich, Peter (Dr.) 
Year:
2021 
Pages:
VI, 59 S. 
Language:
en 
Language from translation:
de 
University:
Technische Universität München 
Faculty:
Fakultät für Informatik