1.1 --- a/paper/src/paper.tex	Sat May 28 18:31:12 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Sun May 29 03:34:06 2011 +0200
     1.3 @@ -1,23 +1,21 @@
     1.4 -\documentclass[10pt, a4paper, onecolumn]{article}
     1.5 -%\usepackage[top=0cm, bottom=0cm, left=0cm, right=0cm]{geometry}
     1.6 -%\usepackage[ngerman]{babel}
     1.7 +\documentclass[ a4paper, pagesize, DIV=calc, smallheadings]{article}  
     1.8  \usepackage{graphicx}
     1.9  %\usepackage[latin1]{inputenc}
    1.10  \usepackage{amsmath, amsthm, amssymb}
    1.11  \usepackage{typearea}
    1.12  \usepackage{algorithm}
    1.13  \usepackage{algorithmic}
    1.14 +%\usepackage[T1]{fontenc}
    1.15 +%\usepackage{arev}
    1.16  
    1.17  \pagestyle{headings}
    1.18  \renewcommand{\familydefault}{\sfdefault}
    1.19 -\title{\textbf{Verification of Reactive Systems}}
    1.20 -%\title{\textbf{An Extension of Linear Temporal Logic}}
    1.21 -%\title{\textbf{Verification of Concurrent Systems}}
    1.22 -%\title{\textbf{Temporal Reasoning}}
    1.23 -\author{Eugen Sawin\\   
    1.24 -  University of Freiburg, Germany\\\\
    1.25 -  \texttt{sawine@informatik.uni-freiburg.de}}
    1.26 -\date{May, 2011}
    1.27 +\title{\uppercase{\textbf{\large{Algorithmic Verification of Reactive Systems}}}}
    1.28 +%\title{\textsc{\large{Algorithmic Verification of Reactive Systems}}}
    1.29 +%\author{\textsc{\small{Eugen Sawin}}\\
    1.30 +\author{\uppercase{\footnotesize{Eugen Sawin}}\\
    1.31 +  \em{\footnotesize{University of Freiburg, Germany}}}
    1.32 +\date{\textsc{\hfill}}
    1.33  \begin{document}
    1.34  
    1.35  \maketitle
    1.36 @@ -38,7 +36,7 @@
    1.37  \newpage
    1.38  \section{Introduction}
    1.39  Program verification is a fundamental area of study in computer science. The broad goal
    1.40 -is to verify whether a program is “correct”—i.e., whether the implementation of a program
    1.41 +is to verify whether a program is ``correct''--i.e., whether the implementation of a program
    1.42  meets its specification. This is, in general, too ambitious a goal and several assumptions
    1.43  have to be made in order to render the problem tractable. In these lectures, we will focus
    1.44  on the verification of finite-state reactive programs. For specifying properties of programs,
    1.45 @@ -70,16 +68,19 @@
    1.46  for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
    1.47  
    1.48  \section{$\omega$-regular Languages}
    1.49 -\section{Linear Temporal Logic}
    1.50  \section{B\"uchi Automata}
    1.51  Automata are good.
    1.52 +\section{Linear Temporal Logic}
    1.53 +
    1.54  \section{Model Checking}
    1.55  \begin{thebibliography}{99}
    1.56 -\bibitem{ref:ltl&büchi} Madhavan Mukund. {\em Linear-Time Temporal Logic and B\"uchi Automata}.
    1.57 +\bibitem{ref:ltl&büchi} 
    1.58 +\textsc{Madhavan Mukund.}
    1.59 +{\em Linear-Time Temporal Logic and B\"uchi Automata}.
    1.60  Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
    1.61  
    1.62  \bibitem{ref:handbook} 
    1.63 -Patrick Blackburn, Frank Wolter and Johan Van Benthem. 
    1.64 +\textsc{Patrick Blackburn, Frank Wolter and Johan Van Benthem.}
    1.65  {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
    1.66  3rd Edition, Elsevier, Amsterdam, 2007.
    1.67  \end{thebibliography}