--- a/prio/Paper/document/root.tex	Mon Dec 03 08:16:58 2012 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-\documentclass[runningheads]{llncs}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{mathpartir}
-\usepackage{tikz}
-\usepackage{pgf}
-%\usetikzlibrary{arrows,automata,decorations,fit,calc}
-%\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
-%\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
-%\usetikzlibrary{matrix}
-\usepackage{pdfsetup}
-\usepackage{ot1patch}
-\usepackage{times}
-%%\usepackage{proof}
-%%\usepackage{mathabx}
-\usepackage{stmaryrd}
-\usepackage{url}
-\usepackage{color}
-\titlerunning{Proving the Priority Inheritance Protocol Correct}
-
-
-\urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastyle}{\normalsize\it}%
-
-
-\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
-\renewcommand{\isasymequiv}{$\dn$}
-\renewcommand{\isasymemptyset}{$\varnothing$}
-\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
-\renewcommand{\isasymiota}{}
-
-\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
-\definecolor{mygrey}{rgb}{.80,.80,.80}
-
-\begin{document}
-
-\title{Priority Inheritance Protocol Proved Correct}
-\author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}
-\institute{PLA University of Science and Technology, China \and 
-           King's College London, United Kingdom}
-\maketitle
-
-\begin{abstract}
-In real-time systems with threads, resource locking and 
-priority sched\-uling, one faces the problem of Priority
-Inversion. This problem can make the behaviour of threads
-unpredictable and the resulting bugs can be hard to find.  The
-Priority Inheritance Protocol is one solution implemented in many
-systems for solving this problem, but the correctness of this solution
-has never been formally verified in a theorem prover. As already
-pointed out in the literature, the original informal investigation of
-the Property Inheritance Protocol presents a correctness ``proof'' for
-an \emph{incorrect} algorithm. In this paper we fix the problem of
-this proof by making all notions precise and implementing a variant of
-a solution proposed earlier. Our formalisation in Isabelle/HOL
-uncovers facts not mentioned in the literature, but also shows how to
-efficiently implement this protocol. Earlier correct implementations
-were criticised as too inefficient. Our formalisation is based on
-Paulson's inductive approach to verifying protocols.\medskip
-
-{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
-real-time systems, Isabelle/HOL
-\end{abstract}
-
-\input{session}
-
-%\bibliographystyle{plain}
-%\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: