\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

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

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

\begin{document}

\title{Kleene Algebra with Tests and Demonic Refinement Algebras}
\author{Alasdair Armstrong \and Victor B. F. Gomes \and Georg Struth}
\maketitle

\begin{abstract}
  We formalise Kleene algebra with tests (KAT) and demonic refinement
  algebra (DRA) with tests in Isabelle/HOL.  KAT is relevant for
  program verification and correctness proofs in the partial
  correctness setting.  DRA targets similar applications in the
  context of total correctness.  Our formalisation contains the two
  most important models of these algebras: binary relations in the
  case of KAT and predicate transformers in the case of DRA.  In
  addition, we derive the inference rules for Hoare logic in KAT and
  its relational model.
\end{abstract}

\tableofcontents

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
