Quelle  root.tex

\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage[T1]{fontenc}
\usepackage{mathtools}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage[numbers]{natbib}

% this should be the last package used
\usepackage{pdfsetup}
\usepackage{doi}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\DeclarePairedDelimiter{\norm}{\lVert}{\rVert}

\begin{document}

\title{A Verified Imperative Implementation of B-Trees}
\author{Niels Mündler}
\date{}
\maketitle

\begin{abstract}
In this work, we use the interactive theorem prover Isabelle/HOL
to verify an imperative implementation of the classical B-tree data structure \cite{DBLP:journals/acta/BayerM72}.
The implementation supports set membership, insertion, deletion, iteration and range 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.
We show the validity of this refinement using
the separation logic utilities from the
Isabelle Refinement Framework \cite{Refine_Imperative_HOL-AFP}. 
The code can be exported to the programming languages SML, Scala and OCaml.
This entry contains two developments:
\begin{itemize}
    \item \emph{B-Trees} This formalisation is discussed in greater detail in the corresponding Bachelor's Thesis\cite{BTNielsMuendler}.
    \item \emph{B$^+$-Trees} This formalisation also supports range queries and is discussed in a paper published at ICTAC 2022.
\end{itemize}
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
{\raggedright
\bibliographystyle{plainnat}
\bibliography{root}
}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: