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

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

\usepackage{amsmath}
\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

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

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

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles}
\author{Albert Rizaldi, Fabian Immler}
\maketitle

\begin{abstract}
The Vienna Convention on Road Traffic defines the safe distance traffic rules
informally.
This could make autonomous vehicle liable for safe-distance-related accidents
because there is no clear definition of how large a safe distance is.
We provide a formally proven prescriptive definition of a safe distance, and
checkers which can decide whether an autonomous vehicle is obeying the safe
distance rule.
Not only does our work apply to the domain of law, but it also serves as a
specification for autonomous vehicle manufacturers and for online verification
of path planners. This formalization accompanies our paper "A Formally Verified Checker of the Safe
Distance Traffic Rules for Autonomous Vehicles".~\cite{NASA/RizaldiImmlerAlthoff16}
\end{abstract}

\tableofcontents

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

% generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

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