\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}

\newcommand\isafor{\textsf{IsaFoR}}
\newcommand\ceta{\textsf{Ce\kern-.18emT\kern-.18emA}}

\begin{document}

\title{Executable Transitive Closures of Finite Relations\footnote{Supported by FWF (Austrian Science Fund) project P22767-N13.}}
\author{Christian Sternagel and Ren\'e Thiemann}
\maketitle

\begin{abstract}
  We provide a generic work-list algorithm to compute the transitive closure of
  finite relations where only successors of newly detected states are generated.
  This algorithm is then instantiated for lists over arbitrary carriers and red
  black trees \cite{rbt} (which are faster but require a linear order on the
  carrier), respectively. 

  Our formalization was performed as part of the \isafor/\ceta{} project%
  \footnote{\url{http://cl-informatik.uibk.ac.at/software/ceta}} \cite{CeTA},
  where reflexive transitive closures of large tree automata have to be
  computed.
\end{abstract}

\tableofcontents


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



\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
