diff -r 8057b328e9d3 -r bcbcdb92089f paper/src/paper.tex
--- a/paper/src/paper.tex	Sat May 28 18:31:12 2011 +0200
+++ b/paper/src/paper.tex	Sun May 29 03:34:06 2011 +0200
@@ -1,23 +1,21 @@
-\documentclass[10pt, a4paper, onecolumn]{article}
-%\usepackage[top=0cm, bottom=0cm, left=0cm, right=0cm]{geometry}
-%\usepackage[ngerman]{babel}
+\documentclass[ a4paper, pagesize, DIV=calc, smallheadings]{article}  
 \usepackage{graphicx}
 %\usepackage[latin1]{inputenc}
 \usepackage{amsmath, amsthm, amssymb}
 \usepackage{typearea}
 \usepackage{algorithm}
 \usepackage{algorithmic}
+%\usepackage[T1]{fontenc}
+%\usepackage{arev}
 
 \pagestyle{headings}
 \renewcommand{\familydefault}{\sfdefault}
-\title{\textbf{Verification of Reactive Systems}}
-%\title{\textbf{An Extension of Linear Temporal Logic}}
-%\title{\textbf{Verification of Concurrent Systems}}
-%\title{\textbf{Temporal Reasoning}}
-\author{Eugen Sawin\\   
-  University of Freiburg, Germany\\\\
-  \texttt{sawine@informatik.uni-freiburg.de}}
-\date{May, 2011}
+\title{\uppercase{\textbf{\large{Algorithmic Verification of Reactive Systems}}}}
+%\title{\textsc{\large{Algorithmic Verification of Reactive Systems}}}
+%\author{\textsc{\small{Eugen Sawin}}\\
+\author{\uppercase{\footnotesize{Eugen Sawin}}\\
+  \em{\footnotesize{University of Freiburg, Germany}}}
+\date{\textsc{\hfill}}
 \begin{document}
 
 \maketitle
@@ -38,7 +36,7 @@
 \newpage
 \section{Introduction}
 Program verification is a fundamental area of study in computer science. The broad goal
-is to verify whether a program is “correct”—i.e., whether the implementation of a program
+is to verify whether a program is ``correct''--i.e., whether the implementation of a program
 meets its specification. This is, in general, too ambitious a goal and several assumptions
 have to be made in order to render the problem tractable. In these lectures, we will focus
 on the verification of finite-state reactive programs. For specifying properties of programs,
@@ -70,16 +68,19 @@
 for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
 
 \section{$\omega$-regular Languages}
-\section{Linear Temporal Logic}
 \section{B\"uchi Automata}
 Automata are good.
+\section{Linear Temporal Logic}
+
 \section{Model Checking}
 \begin{thebibliography}{99}
-\bibitem{ref:ltl&büchi} Madhavan Mukund. {\em Linear-Time Temporal Logic and B\"uchi Automata}.
+\bibitem{ref:ltl&büchi} 
+\textsc{Madhavan Mukund.}
+{\em Linear-Time Temporal Logic and B\"uchi Automata}.
 Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
 
 \bibitem{ref:handbook} 
-Patrick Blackburn, Frank Wolter and Johan Van Benthem. 
+\textsc{Patrick Blackburn, Frank Wolter and Johan Van Benthem.}
 {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
 3rd Edition, Elsevier, Amsterdam, 2007.
 \end{thebibliography}