\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}

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

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

% Tweaks
\newcounter{TTStweak_tag}
\setcounter{TTStweak_tag}{0}
\newcommand{\setTTS}{\setcounter{TTStweak_tag}{1}}
\newcommand{\resetTTS}{\setcounter{TTStweak_tag}{0}}
\newcommand{\insertTTS}{\ifnum\value{TTStweak_tag}=1 \ \ \ \fi}

\renewcommand{\isakeyword}[1]{\resetTTS\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
\renewcommand{\isachardoublequoteopen}{\insertTTS}
\renewcommand{\isachardoublequoteclose}{\setTTS}
\renewcommand{\isanewline}{\mbox{}\par\mbox{}\resetTTS}

\renewcommand{\isamarkupcmt}[1]{\hangindent5ex{\isastylecmt --- #1}}


\begin{document}

\title{A Fully Verified Executable LTL Model Checker}
\author{Javier Esparza, Peter Lammich, Ren\'{e} Neumann, Tobias Nipkow,\\Alexander Schimpf, Jan-Georg Smaus}

\maketitle

\begin{abstract}
We present an LTL model checker whose code has been completely verified using
the Isabelle theorem prover. The checker consists of over 4000 lines of
ML code. The code is produced using the Isabelle Refinement
Framework, which allows us to split its correctness proof into (1) the proof
of an abstract version of the checker, consisting of a few hundred lines of
``formalized pseudocode'', and (2) a verified refinement step in which mathematical sets and
other abstract structures are replaced by implementations of efficient
structures like red-black trees and functional arrays. This leads to a checker that,
while still slower than unverified checkers, can already be used as a trusted
reference implementation against which advanced implementations can be
tested.

An early version of this model checker is described elsewhere~\cite{VeriLTLMC13}.
\end{abstract}

\clearpage

\tableofcontents

\clearpage

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

% generated text of all theories
\input{session}

\clearpage

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

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