\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage[english]{babel}

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

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

\newcommand{\etal}{\emph{et al.}}
\newcommand{\keyword}[1]{\ensuremath{\textsf{\textbf{#1}}}}
\newcommand{\Klemma}{\keyword{lemma}}
\newcommand{\Ktheorem}{\keyword{theorem}}
\newcommand{\Kif}{\keyword{if}}
\newcommand{\Klet}{\keyword{let}}
\newcommand{\Kleft}{\boldsymbol \leftarrow}
\newcommand{\Kdo}{\keyword{do}}
\newcommand{\Kin}{\keyword{in}}
\newcommand{\Kthen}{\keyword{then}}
\newcommand{\Kelse}{\keyword{else}}

\newcommand{\identifier}[1]{\textsl{\textsf{#1}}}
\newcommand{\Iaexp}{\identifier{aexp}}
\newcommand{\IAffine}{\identifier{Affine}}
\newcommand{\IAffines}{\identifier{Affines}}
\newcommand{\Iaffineofivl}{\identifier{affine-of-ivl}}
\newcommand{\IAdd}{\identifier{Add}}
\newcommand{\Iaddaffine}{\identifier{add-affine}}
\newcommand{\IAddE}{\identifier{AddE}}
\newcommand{\IBasis}{\identifier{Basis}}
\newcommand{\Ibinop}{\identifier{binop}}
\newcommand{\Ibox}{\identifier{box}}
\newcommand{\Icenter}{\identifier{center}}
\newcommand{\Icoeff}{\identifier{coeff}}
\newcommand{\Icoeffs}{\identifier{coeffs}}
\newcommand{\Iapprox}{\identifier{approx}}
\newcommand{\ID}{\identifier{D}}
\newcommand{\Ideg}{\identifier{deg}}
\newcommand{\Idim}{\identifier{dim}}
\newcommand{\Idivl}{\identifier{div}^-}
\newcommand{\Idivr}{\identifier{div}^+}
\newcommand{\Ieexp}{\identifier{eexp}}
\newcommand{\IElem}{\identifier{elem}}
\newcommand{\Ieulerseries}{\identifier{euler-series}}
\newcommand{\Ieulerstep}{\identifier{euler-step}}
\newcommand{\Ifalse}{\identifier{False}}
\newcommand{\Ifilter}{\identifier{filter}}
\newcommand{\Ifold}{\identifier{fold}}
\newcommand{\Ifor}{\identifier{for}}
\newcommand{\Ifst}{\identifier{fst}}
\newcommand{\IFloat}{\identifier{Float}}
\newcommand{\Iindices}{\identifier{indices}}
\newcommand{\IInverse}{\identifier{Inverse}}
\newcommand{\Iinverseaffine}{\identifier{inverse-affine}}
\newcommand{\Iivp}{\identifier{ivp}}
\newcommand{\Ilen}{\identifier{len}}
\newcommand{\Imap}{\identifier{map}}
\newcommand{\Imerge}{\identifier{merge}}
\newcommand{\IMinus}{\identifier{Minus}}
\newcommand{\Iminusaffine}{\identifier{minus-affine}}
\newcommand{\IMult}{\identifier{Mult}}
\newcommand{\Imultaffine}{\identifier{mult-affine}}
\newcommand{\INone}{\identifier{None}}
\newcommand{\INum}{\identifier{Num}}
\newcommand{\Irad}{\identifier{rad}}
\newcommand{\Iradup}{\identifier{rad}^+}
\newcommand{\Iround}{\identifier{round}}
\newcommand{\IScale}{\identifier{Scale}}
\newcommand{\Iscaleaffine}{\identifier{scale-affine}}
\newcommand{\Isol}{\identifier{sol}}
\newcommand{\ISome}{\identifier{Some}}
\newcommand{\Isplit}{\identifier{split}}
\newcommand{\Isummarize}{\identifier{summarize}}
\newcommand{\To}{\Rightarrow}
\newcommand{\Itrue}{\identifier{True}}
\newcommand{\Itruncatedown}{\identifier{trunc}^-}
\newcommand{\Itruncateup}{\identifier{trunc}^+}
\newcommand{\Iroundbinop}{\identifier{round-binop}}
\newcommand{\UNIV}[1]{\mathcal{U}_{#1}}
\newcommand{\Iunzip}{\identifier{unzip}}
\newcommand{\IVar}{\identifier{Var}}
\newcommand{\Izip}{\identifier{zip}}

\newcommand{\Tset}[1]{#1\,\identifier{set}}
\newcommand{\Tlist}[1]{#1\,\identifier{list}}
\newcommand{\Taffine}[1]{#1\,\identifier{affine}}
\newcommand{\Toption}[1]{#1\,\identifier{option}}
\newcommand{\Tbcontfun}[2]{#1\To_{\identifier{bc}}#2}
\newcommand{\Tfinmap}[2]{#1\rightharpoondown_{\identifier{f}}#2}
\newcommand{\Tfilter}[1]{#1\,\identifier{filter}}

\newcommand{\Bool}{\ensuremath{\mathbb{B}}}
\newcommand{\Real}{\ensuremath{\mathbb{R}}}
\newcommand{\Float}{\ensuremath{\mathbb{F}}}
\newcommand{\Eucl}[1]{\ensuremath{\mathbb{R}^{#1}}}
\newcommand{\Complex}{\ensuremath{\mathbb{C}}}
\newcommand{\Nat}{\ensuremath{\mathbb{N}}}
\newcommand{\Integer}{\ensuremath{\mathbb{Z}}}

\newcommand{\ToDO}[1]{{\color{red}\textbf{TODO:} #1}}
\newcommand{\Todo}[1]{{\color{red}[#1]}}

\newcommand{\limseq}{\xrightarrow{\hspace*{2em}}}
\newcommand{\interpret}[1]{\ensuremath{[\![#1]\!]}}

\title{Continuous Systems Reachability using Adaptive Runge-Kutta Methods – Formally Verified}
\author{Fabian Immler}

\begin{document}

\maketitle

\begin{abstract}

Ordinary differential equations (ODEs) are often used to model the dynamics of (often safety-critical)
continuous systems. This work presents the formal verification of an algorithm for reachability analysis in
continuous systems. The algorithm features adaptive Runge- Kutta methods and rigorous numerics based
on affine arithmetic. It is proved to be sound with respect to the existing formalization of ODEs in
Isabelle/HOL. Optimizations like splitting, intersecting and collecting reachable sets are necessary
to analyze chaotic systems. Experiments demonstrate the practical usability of our developments.

\end{abstract}

\section{Relations to the paper}

Here we relate the contents of the submission~\cite{Immler} for CPP~2015 with the sources of our
developments. In the following list we show which notions and theorems in the paper correspond to
which parts of the source code. If you are (still) interested in the relations
to our ITP~2012 paper~\cite{immlerhoelzl}, you should take a look at the document of older releases
(before Isabelle~2013-1) of this AFP entry.

\begin{enumerate}
\item Introduction
\item Main Ideas
\item Verification
  \begin{enumerate}
  \item Reachability in Continuous Systems: Definition \textit{flowsto} in section~\ref{sec:rk-affine}
  \item Rigorous Numerics: Affine Arithmetic: see the separate entry Affine Arithmetic~\cite{Immler2014b}
  \item Guaranteed Runge-Kutta methods:
    \begin{itemize}
    \item Theorem~1: lemma \textit{cert-stepsize-spec} in section~\ref{sec:rk-affine}
    \item Theorem~2: lemma \textit{rk2-remainder-nres-spec} in section~\ref{sec:rk-affine}
    \item Theorem~3: lemma \textit{rk2-step-spec} in section~\ref{sec:rk-affine}
    \end{itemize}
  \item Splitting: Theorem~4: lemma \textit{split-aformE} in section~\ref{sec:aforms}
  \item Reduction of Reachable Sets
    \begin{itemize}
    \item Algorithm~1: definition \textit{rk2-step} in section~\ref{sec:euleraformcode}
    \item Algorithm~3: definition \textit{intersection-iteration-impl} in section~\ref{sec:euleraformcode}
    \item Theorem~5: lemma \textit{intersection-iteration-impl} in section~\ref{sec:rk-affine}
    \end{itemize}
  \item Summarization of Intersections: Theorem~6: lemma \textit{partition-overappr} in section~\ref{sec:rk-affine}
  \item Reachability Analysis
    \begin{itemize}
    \item Theorem~7: lemma \textit{resolve-sctn} in section~\ref{sec:rk-affine}
    \item Algorithm~4: definition \textit{resolve-sctn} in section~\ref{sec:euleraformcode}
    \item Algorithm~5: definition \textit{poincare-distance-d} in section~\ref{sec:euleraformcode}
    \item Theorem~8: lemma \textit{poincare-distance-d} in section~\ref{sec:rk-affine}
    \end{itemize}
  \end{enumerate}
\item Implementation
\item Experiments
  \begin{itemize}
  \item Van-der-Pol: section~\ref{sec:vanderpol}
  \item Lorenz: section~\ref{sec:lorenz}
  \end{itemize}
\item Conclusion
\end{enumerate}

\tableofcontents

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

% generated text of all theories
\input{session}

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

\end{document}

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