doc: Fix university name and credit BRICKS/FOCUS project.

Ignore-this: 5627502dd551b7c29e383bd26bb96246 darcs-hash:20100201111628-bab43-f2099273d43230bcaee67fe50c8af341708d75b8.gz
Eelis · Feb 1, 2010 · 1739f5f · 1739f5f
1 parent 6e7d480
commit 1739f5f
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/doc/paper.tex b/doc/paper.tex
@@ -116,8 +116,8 @@
 \title{\thetitle}
 \subtitle{An Implementation of the Abstraction Method In Coq}
 
-\author{}
-\institute{Institute for Computing and Information Sciences\\ Nijmegen University}
+\author{\eelis}
+\institute{Institute for Computing and Information Sciences\\ Raboud University Nijmegen}
 
 \begin{document}
 
@@ -127,7 +127,8 @@
 %\titlerunning{\em}
 
 \begin{abstract}
-This technical report documents our development of a hybrid system safety prover, implemented in Coq using the abstraction method introduced by Alur in \cite{alur}. The development includes: a formalization of the structure of hybrid systems; a systematic approach and generic set of support utilities for the construction of an abstract system (consisting of decidable ``overestimators'' of abstract transitions and initiality) faithfully representing a (concrete) hybrid system; a translation of abstract systems to graphs enabling decision of abstract state reachability using a certified graph reachability algorithm; a proof of an example hybrid system (taken from \cite{alur}) generated using this tool stack. The development critically relies on the computable real number implementation part of the C-CoRN library of formalized constructive mathematics. \todo{Hm, anything else worth mentioning?}
+This technical report documents our development of a hybrid system safety prover, implemented in Coq using the abstraction method introduced by Alur in \cite{alur}. The development includes: a formalization of the structure of hybrid systems; a systematic approach and generic set of support utilities for the construction of an abstract system (consisting of decidable ``overestimators'' of abstract transitions and initiality) faithfully representing a (concrete) hybrid system; a translation of abstract systems to graphs enabling decision of abstract state reachability using a certified graph reachability algorithm; a proof of an example hybrid system (taken from \cite{alur}) generated using this tool stack. The development critically relies on the computable real number implementation part of the C-CoRN library of formalized constructive mathematics. \todo{Hm, anything else worth mentioning?}\footnote{This research was supported by the BRICKS/FOCUS project 642.000.501 ``Advancing the Real use of Proof Assistants''.}
+
 
 \end{abstract}