1\documentclass[11pt,a4paper]{article}
2\usepackage{isabelle,isabellesym}
3
4\usepackage{amssymb}
5\usepackage[english]{babel}
6\usepackage[utf8]{inputenc}
7\usepackage[only,bigsqcap]{stmaryrd}
8\usepackage{eufrak}
9\usepackage{textcomp}
10
11% this should be the last package used
12\usepackage{pdfsetup}
13
14% urls in roman style, theory text in math-similar italics
15\urlstyle{rm}
16
17% for rule output in LaTeXsugar
18\usepackage{mathpartir}
19\usepackage{graphicx}
20\isabellestyle{it}
21
22% this should be the last package used
23\usepackage{pdfsetup}
24
25\renewcommand{\isasymacute}{\isatext{\'\relax\hspace{-0.20em}}}
26\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup\relax\hspace{-0.15em}}
27
28\begin{document}
29
30\title{--- \textbf{Simpl} --- \\
31       A Sequential Imperative Programming Language\\
32       Syntax, Semantics, Hoare Logics and Verification Environment}
33\author{Norbert W. Schirmer}
34
35\begin{abstract}
36We present the theory of Simpl, a sequential imperative programming language.
37We introduce its syntax, its semantics (big and small-step operational
38semantics) and Hoare logics for both partial as well as total correctness.
39We prove soundness and completeness of the Hoare logic. We
40integrate and automate the Hoare logic in Isabelle/HOL to obtain a
41practically usable verification environment for imperative programs.
42
43Simpl is independent of a concrete programming language but expressive
44enough to cover all common language features: mutually recursive
45procedures, abrupt termination and exceptions, runtime faults, local
46and global variables, pointers and heap, expressions with side
47effects, pointers to procedures, partial application and closures,
48dynamic method invocation and also unbounded nondeterminism.
49\end{abstract}
50
51\maketitle
52
53\tableofcontents
54\parindent 0pt\parskip 0.5ex
55
56\pagebreak
57
58\begin{center}
59  \makebox[0pt]{\includegraphics[width=\paperwidth=\textheight,keepaspectratio]{session_graph}
60}\end{center}
61
62\pagebreak
63
64\section{Introduction}
65
66The work presented in these theories was developed within the German Verisoft
67project\footnote{\url{http://www.verisoft.de}}. A thorough description of the core
68parts can be found in my PhD thesis~\cite{Schirmer-PhD}. A tutorial-like user guide
69is in Section~\ref{sec:UserGuide}.
70
71Applications so far include BDD-normalisation~\cite{Ortner-Schirmer-TPHOL05},
72a C0 compiler~\cite{Leinenbach:SSV08-??}, a page fault handler~\cite{Alkassar:TACAS08-??}
73and extensions towards separation logic~\cite{Tuch:separation-logic:2007}.
74
75
76% generated text of all theories
77\input{session}
78
79% optional bibliography
80\bibliographystyle{abbrv}
81\bibliography{root}
82
83\end{document}
84
85%%% Local Variables:
86%%% mode: latex
87%%% TeX-master: t
88%%% End:
89