Delete a lot of tex stuff, better debug info

Some other stuff, too, I think. Oh well. No biggie!

1 files changed, 0 insertions, 780 deletions

diff --git a/tex/presentation/thomas/slides.tex b/tex/presentation/thomas/slides.tex
deleted file mode 100644
index 83aa35b..0000000
--- a/tex/presentation/thomas/slides.tex
+++ /dev/null
@@ -1,780 +0,0 @@
-\newcommand{\brighten}{\pos{0,0}{\begin{tikzpicture}[fill opacity=.5, opacity=.5]\pgfsetstrokecolor{white}\filldraw[fill=white] (0,0) rectangle (14,12);\end{tikzpicture}}}
-
-\newcommand{\stmtone}{(\vx_1,\vx_2) := (0,1)}
-\newcommand{\stmttwo}{\vx_1 \leq 8 ;\, (\vx_1,\vx_2) := (\vx_1 + 2, \vx_2 + 2)}
-
-%%%
-%%%
-%%%
-
-\title{{\bf Static Analysis \\ through \\Abstract Interpretation, \\Convex Optimization, and\\ Strategy Iteration}}
-
-\author{
-  {\bf Thomas Martin Gawlitza${}^1$}
-  \\[3pt]
-  joint work with
-  \\[3pt]
-  {\bf Helmut Seidl${}^2$}
-}
-
-\institute{
-  $\fourIdx{\text{{\large\bf 1}}}{}{}{}{\text{\includegraphics[height=15mm]{../logos/usyd.pdf}}}$
-  \qquad\qquad
-  $\fourIdx{\text{{\large\bf 2}}}{}{}{}{\text{\includegraphics[height=15mm]{../logos/TUM.pdf}}}$
-}
-
-\date{\bf SAPLING Meeting, November 2011}
-
-%%%
-%%%
-%%%
-
-\newcommand\partone{Abstract Interpretation using Zones}
-\newcommand\parttwo{Max-Strategy Iteration}
-\newcommand\partthree{Conclusion}
-
-\newcommand{\outline}[1]{
-	\frame{\Large\bf
-	\frametitle{Outline}
-	\begin{enumerate}
-	  \item 
-	    \ifthenelse{\equal{#1}{1}}%
-	    {\partone}%
-	    {\Grey{\partone}}
-	  \bigskip
-	  \bigskip
-	  \item 
-	    \ifthenelse{\equal{#1}{2}}%
-	    {\bf \parttwo}%
-	    {\bf\Grey{\parttwo}}
-	  \bigskip
-	  \bigskip
-	  \item 
-	    \ifthenelse{\equal{#1}{3}}%
-	    {\bf\partthree}%
-	    {\Grey{\partthree}}
-	\end{enumerate}
-	}
-	\ifthenelse{\equal{#1}{1}}{\section{\partone}}{}
-	\ifthenelse{\equal{#1}{2}}{\section{\parttwo}}{}
-	\ifthenelse{\equal{#1}{3}}{\section{\partthree}}{}
-}
-
-%%%
-%%%
-%%%
-
-\section{Title}
-
-%%%
-
-\frame[plain]{\titlepage}
-
-%%%
-
-\outline{1}
-
-%%%
-
-\begin{frame}{Abstract Domain: {\bf Zones} (1/2)}
-\uncover<2->{
-      \Green{\bf Goal}: \emph{Tight bounds} on the possible values of \emph{integer variables}
-      
-      \qquad\qquad (like $\vx_1 \leq 42, \; \vx_2 \leq 13$)
-
-      \bigskip
-      \qquad$\leadsto$ buffer overflows, worst-case execution times, etc.
-}
-      
-\uncover<3->{
-      \bigskip
-      \Green{\bf Definition}:
-      Invariants of the form 
-      \begin{align*}
-        \bigwedge_\vx \vx \leq b_{\vx} \wedge \bigwedge_\vx -\vx \leq b_{-\vx} \wedge \bigwedge_{\vx,\vy} \vx - \vy \leq b_{\vx-\vy}
-      \end{align*}
-      
-      That is:
-               \emph{bounds} on \emph{variables} and
-                \emph{differences of variables}.
-}    
-
-\uncover<4->{
-      \bigskip
-      \Green{\bf Applications}:
-
-      \smallskip
-      Model-checking of timed automata \cite{DBLP:conf/eef/Yovine96,DBLP:conf/rtss/LarsenLPY97}
-      
-      \smallskip
-      Static program analysis \cite{Sagiv01,DBLP:conf/pado/Mine01}
-}
-
-\end{frame}
-
-%%%
-
-\begin{frame}{Abstract Domain: {\bf Zones} (2/2)}
-\uncover<2->{
-    \Green{\bf Our point of view}:
-    Zones are special \emph{template polyhedra}
-    
-    \smallskip
-    \qquad$\leadsto$ template polyhedra: \cite{DBLP:conf/vmcai/SankaranarayananSM05}
-}    
- 
-\uncover<3->{   
-    \bigskip
-    \Green{\bf Given}: 
-    \emph{template constraint matrix} $T \in \{-1,0,1\}^{m\times n}$, where every row contains 
-               \emph{at most one $1$}, and 
-               \emph{at most one $-1$}. 
-               Then:
-\begin{align*}
-  \gamma(b) 
-    &:= 
-    \{ x \in \Z^n \mid T x \leq b \}
-    && 
-    \text{for all } b \in \CZ^m
-  \\
-  \alpha(X) 
-    &:= 
-    \min \; \{ b \in \CZ^m \mid \gamma(b) \supseteq X \}
-    && 
-    \text{for all } X \subseteq \Z^n
-\end{align*}	
-}
-
-\uncover<4->{
-  \Green{\bf Example}:
-  Let
-  $
-    T
-    =
-	      \begin{pmatrix}
-	        1 & 0 \\
-	        0 & 1 \\
-	        -1 & 1
-	      \end{pmatrix}
-  $.
-  Then:
-
-  $
-  \gamma\left(
-    \begin{pmatrix} 3 \\ 2 \\ 1 \end{pmatrix}
-  \right)
-  =
-  \left\{
-    \begin{pmatrix} \vx_1 \\ \vx_2 \end{pmatrix} \in \Z^2 
-    \mid 
-    T \begin{pmatrix} \vx_1 \\ \vx_2 \end{pmatrix} 
-    \leq 
-    \begin{pmatrix} 3 \\ 2 \\ 1 \end{pmatrix}
-  \right\}
-  =
-  \begin{matrix}\mbox{\scalebox{0.5}{
-  \begin{tikzpicture}[show background grid,scale=1]
-    \filldraw[fill=lightgray,color=lightgray] 
-      (-1,-1) -- (0-1,1-1) -- (1,2) -- (3,2) -- (3,-1) -- (-1,-1);
-    \draw[thick, ->] (-1,0) -- (4.2,0) node[right] {$\vx_1$-axis};
-    \draw[thick, ->] (0,-1) -- (0,3.2) node[above] {$\vx_2$-axis};
-    \draw[ultra thick] (-1,2) -- (4,2) node[above] {$\vx_2 \leq 2$};
-    \draw[ultra thick] (-1,0) -- (2,3) node[above,xshift=2mm] {$\vx_2 \leq 1 {+} \vx_1$};
-    \draw[ultra thick] (3,-1) -- (3,3) node[right] {$\vx_1 \leq 3$};
-  \end{tikzpicture}}}\end{matrix}
-  $
-}
-\end{frame}
-
-%%%
-
-\begin{frame}{Zone-based Static Program Analysis}
-\uncover<2->{
-  \Green{\bf Goal}: 
-  Find minimal \emph{zones} that are \emph{invariants}
-}
- 
-\uncover<3->{ 
-  \bigskip
-  \Green{\bf Example}:
-  \begin{center}
-        
-	$
-	\begin{matrix}\mbox{\scalebox{0.8}{\begin{tikzpicture}
-		 \node (start) [circle,draw] {$a$};
-		 \node (null) [coordinate,right of = start] {};
-		 \node (n1) [below of = start,circle,draw,yshift=-8mm]{$b$};
-		 \path[ultra thick,->] (null) edge [] node [right] {} (start);
-		 \path[ultra thick,->] (start) edge [] node [right,yshift=1mm] {$\stmtone$} (n1);
-		 \path[ultra thick,->] (n1) edge [loop right,out=35,in=-35, distance=20mm] node [right] {
-		   $\stmttwo$
-		 } (n1);
-	\end{tikzpicture}}}\end{matrix}
-	\qquad\quad
-	T 
-	=
-	      \begin{pmatrix}
-	        1 & 0 \\
-	        0 & 1 \\
-	        -1 & 1
-	      \end{pmatrix}
-	$
-  \end{center}
-}
-
-\uncover<4->{
-  \vspace*{-5mm}
-  For program point $a$:
-
-  \smallskip
-  $
-    \gamma \left( 
-      \begin{pmatrix} \infty \\ \infty \\ \infty \end{pmatrix} 
-    \right)
-    =
-    \left\{ 
-      \begin{pmatrix} \vx_1\\\vx_2 \end{pmatrix} 
-      \mid
-	      \begin{pmatrix}
-	        1 & 0 \\
-	        0 & 1 \\
-	        -1 & 1
-	      \end{pmatrix}
-      \begin{pmatrix} \vx_1\\\vx_2 \end{pmatrix} 
-      \leq 
-      \begin{pmatrix} \infty \\ \infty \\ \infty \end{pmatrix}            
-    \right\}
-  $
-}
-
-\uncover<5->{ 
-  \bigskip
-  For program point $b$:
-
-  \smallskip
-  $
-    \gamma \left( 
-      \begin{pmatrix} 10 \\ 11 \\ 1 \end{pmatrix} 
-    \right)
-    =
-    \left\{ 
-      \begin{pmatrix} \vx_1\\\vx_2 \end{pmatrix} 
-      \mid
-	      \begin{pmatrix}
-	        1 & 0 \\
-	        0 & 1 \\
-	        -1 & 1
-	      \end{pmatrix}
-      \begin{pmatrix} \vx_1\\\vx_2 \end{pmatrix} 
-      \leq 
-      \begin{pmatrix} 10 \\ 11 \\ 1 \end{pmatrix}            
-    \right\}
-  $
-}
-\end{frame}
-
-%%%
-
-\begin{frame}{How Can We Compute {\bf Small} Zones?}
-  \begin{enumerate}
-    \item<2->
-    À la \cite{Sagiv01,DBLP:conf/pado/Mine01}
-  
-    \smallskip
-    Abstr.\ Interpr.\ / widening / narrowing à la \cite{DBLP:conf/popl/CousotC77}
-    
-    \smallskip
-    \uncover<3->{\emph{Properties}:}
-    \begin{itemize}
-      \smallskip\item<4->
-        Abstract transformers can be implemented in \emph{strongly polynomial time}
-        (based on the Floyd-Warshall algorithm)
-      \smallskip\item<5->
-        \emph{Best} abstract transformers only for special classes of affine assignments 
-        (like $\vx = \vx + d$ and $\vx = \vy + d$).
-       \smallskip\item<6->
-         Computed zones are \emph{not} necessarily \emph{minimal} 
-    \end{itemize}
-    \bigskip\item<7->
-    À la \cite{DBLP:conf/csl/GawlitzaS07}
-  
-    \smallskip
-    Abstr.\ Interpr.\ / strategy iteration for \emph{template polyhedra}
-    
-    \smallskip
-    \uncover<8->{\emph{Properties}:}
-    \begin{itemize}
-      \smallskip\item<9->
-         Computed the \emph{minimal} zones that are invariant
-      \smallskip\item<10->
-         Arbitrary affine assignments (like $\vx = c_1 \vx_1 + \cdots + c_k \vx_k + d$)
-      \smallskip\item<11->
-         Proves that the corresponding decision problem is in $\mathbf{coNP}$.
-           
-         \qquad (it is also at least as hard as mean payoff games)
-       \smallskip\item<12->
-         At most exp. many iterations, each of which can be performed in \emph{weakly polynomial time} through \emph{linear programming}.
-    \end{itemize}
-  \end{enumerate}
-\end{frame}
-
-%%%
-
-\begin{frame}{Obvious Question}
-  \begin{center}
-    \huge
-    \uncover<2->{Can we do better?}
-  \end{center}
-
-  \begin{center}  
-\uncover<3->{
-  \bigskip
-  \Green{\bf\huge Idea} 
-  
-  \bigskip
-  max-strategy improvement algorithm for \emph{template polyhedra}
-  
-  \vspace*{-2mm}
-  \scalebox{2}{\rotatebox{-90}{$\leadsto$}}
-  
-  \smallskip
-  max-strategy improvement algorithm for \emph{zones}
-}
-
-\uncover<4->{
-  \bigskip
-  \bigskip
-  \Green{\bf\huge Hope} 
-  
-  \bigskip
-  improvement step in \emph{weakly} polynomial time
-  
-  \vspace*{-2mm}
-  \scalebox{2}{\rotatebox{-90}{$\leadsto$}}
-  
-  \smallskip
-  improvement step in \emph{strongly} polynomial time
-}
-  \end{center}
-\end{frame}
-
-%%%
-
-\outline{2}
-
-%%%
-
-\begin{frame}{Abstract Transformers}
-  \uncover<2->{
-      \emph{Statements} %
-      %
-      \begin{align*}
-        T \vx \leq c \; \wedge \;  \vx' = A \vx + d
-      \end{align*}
-}      
-
-\uncover<3->{
-      \emph{Collecting Semantics} %
-      %
-      \begin{align*}
-        \sem{T \vx \leq c \; \wedge \;  \vx' = A \vx + d} (X) 
-        =
-        \{ x' \mid x \in X \wedge Tx \leq c \wedge x' = Ax+d \} 
-      \end{align*}
-}
-
-\uncover<4->{
-      \emph{Abstract Semantics} %
-      %
-      \begin{align*}
-        \sem{T \vx \leq c \; \wedge \;  \vx' = A \vx + d}^\sharp (b)
-          &= \alpha(\sem{T \vx \leq c \; \wedge \;  \vx' = A \vx + d} (\gamma( b )))
-      \end{align*}
-}
-\end{frame}
-
-%%%
-
-\begin{frame}{First Step: {\bf Constraint System} over $\CZ$}
-  
-  \pos{1,1.0}{
-	$
-	\begin{matrix}\mbox{\scalebox{1}{\begin{tikzpicture}
-		 \node (start) [circle,draw] {$a$};
-		 \node (null) [coordinate,right of = start] {};
-		 \node (n1) [below of = start,circle,draw,yshift=-8mm]{$b$};
-		 \uncover<2->{\path[ultra thick,->] (null) edge [] node [right] {} (start);}
-		 \uncover<6->{\path[ultra thick,->] (start) edge [] node [right,yshift=1mm] {$\stmtone$} (n1);}
-		 \uncover<10->{\path[ultra thick,->] (n1) edge [loop right,out=35,in=-35, distance=20mm] node [right] 
-		   {$\stmttwo$} (n1);}
-	\end{tikzpicture}}}\end{matrix}	
-	\qquad
-	T 
-	=
-	      \begin{pmatrix}
-	        1 & 0 \\
-	        0 & 1 \\
-	        -1 & 1
-	      \end{pmatrix}
-	$
-  }
-
-  \pos{0.3,4}{\Green{\bf Least Solution of}}
-  
-  \pos{0.3,4.5}{
-  $
-    \begin{array}{@{}r@{}l}
-    \uncover<3->{\vb^a_{1} &\geq \infty \\}
-    \uncover<4->{\vb^a_{2} &\geq \infty \\}
-    \uncover<5->{\vb^a_{3} &\geq \infty}
-    \\[5pt]
-    \uncover<7->{\vb^b_{1} &\geq \pi_{1}(\sem{\stmtone}^\sharp (\vb^a_{1}, \vb^a_{2}, \vb^a_{3})) \\}
-    \uncover<8->{\vb^b_{2} &\geq \pi_{2}(\sem{\stmtone}^\sharp (\vb^a_{1}, \vb^a_{2}, \vb^a_{3})) \\}
-    \uncover<9->{\vb^b_{3} &\geq \pi_{3}(\sem{\stmtone}^\sharp (\vb^a_{1}, \vb^a_{2}, \vb^a_{3}))}
-    \\[5pt]
-    \uncover<11->{\vb^b_{1} &\geq \pi_{1}(\sem{\stmttwo}^\sharp (\vb^b_{1}, \vb^b_{2}, \vb^b_{3})) \\}
-    \uncover<12->{\vb^b_{2} &\geq \pi_{2}(\sem{\stmttwo}^\sharp (\vb^b_{1}, \vb^b_{2}, \vb^b_{3})) \\}
-    \uncover<13->{\vb^b_{3} &\geq \pi_{3}(\sem{\stmttwo}^\sharp (\vb^b_{1}, \vb^b_{2}, \vb^b_{3})) }
-    \end{array}
-  $
-  }
-\end{frame}
-
-%%%
-
-\begin{frame}{Properties of the Abstract Semantics}
-  \Green{\bf Observation}:
-  %
-  \only<1-10>{%
-      \begin{align*}
-         &\pi_{k}(\sem{T \vx \leq c \; \wedge \;  \vx' = A \vx + d}^\sharp (b)) \\
-         \uncover<2->{=\;& \pi_{k}( \alpha(\sem{T \vx \leq c \; \wedge \;  \vx' = A \vx + d} (\gamma( b ))) ) \\}
-         \uncover<3->{=\;& \pi_{k}( \alpha(\sem{T \vx \leq c \; \wedge \;  \vx' = A \vx + d} ( \{ \vx \in \Z^n \mid T\vx \leq b \} )) ) \\}
-         \uncover<4->{=\;& \pi_{k}( \alpha( \{ \vx' \mid \vx, \vx' \in \Z^n \;\wedge\; T \vx \leq b, c \; \wedge \;  \vx' = A \vx + d \} ) ) \\}
-         \uncover<5->{=\;& \pi_{k}( \alpha( \{ A \vx + d \mid \vx \in \Z^n \;\wedge\; T \vx \leq \min(b, c)  \} ) ) \\}
-         \uncover<6->{=\;& \sup \; \{ T_k(A \vx + d) \mid \vx \in \Z^n \;\wedge\; T \vx \leq \min(b, c)  \} \\}
-         \uncover<7->{=\;& T_k d + \sup \; \{ T_k A \vx \mid \vx \in \Z^n \;\wedge\;  T \vx \leq \min ( b, c )  \}  \\}
-         \uncover<8->{=\;& T_k d + \sup \; \{ T_k A \vx \mid \vx \in \R^n \;\wedge\;  T \vx \leq \min ( b, c )  \}  \\}
-         \uncover<9->{=\;& T_k d + \inf \; \{ (\min( b, c ))^\top \vy \mid \vy \in \R_{\geq 0}^n \wedge T^\top \vy = (T_1A)^\top \vy  \}  \\}
-         \uncover<10->{=\;& T_k d + \inf \; \{ (\min( b, c ))^\top \vy \mid \vy \in \Z_{\geq 0}^n \wedge T^\top \vy = (T_1A)^\top \vy  \}  \\}
-      \end{align*}%
-  }%
-  \only<11->{%
-      \begin{align*}
-         &\pi_{k}(\sem{T \vx \leq c \; \wedge \;  \vx' = A \vx + d}^\sharp (b)) \\
-         \uncover<10->{=\;& T_k d + \inf \; \{ (\min( b, c ))^\top \vy \mid \vy \in \Z_{\geq 0}^n \wedge T^\top \vy = (T_1A)^\top \vy  \}  \\}
-      \end{align*}
-  }%
-      
-   \uncover<12->{
-      \Green{\bf Consequences}:
-      
-      \bigskip
-      $\pi_k \circ \sem{T \vx \leq c \; \wedge \;  \vx' = A \vx + d}^\sharp : \CZ^m \to \CZ$
-      \begin{enumerate}
-        \smallskip\item<13->
-          is a point-wise \emph{minimum} of finitely many \emph{monotone} and \emph{affine} functions from the set $\CZ^M \to \CZ$.
-        \smallskip\item<14->
-          can be evaluated in \emph{strongly polynomial time}.
-          
-          \smallskip
-            \qquad$\leadsto$ minimum cost flow network problem
-            
-            \qquad$\leadsto$ $\mathcal{O}( m \cdot \log m \cdot ( n + m \cdot \log m ))$
-      \end{enumerate}
-    }
-    
-%    \uncover<15>{
-%      \bigskip
-%      \Green{\bf So What?}
-%    }
-\end{frame}
-
-%%%
-
-\begin{frame}{Minimum Cost Flow Network Problem}
-  \begin{align*}
-    \min  \;\; b^\top \begin{pmatrix} \vy_1 \\ \vy_2 \\ \vy_3 \end{pmatrix} 
-    \qquad\qquad
-    \\[10pt]
-    %
-	      \begin{pmatrix}
-	        1 & 0 & -1 \\
-	        0 & 1 & 1\\
-	        -1 & -1 & 0
-	      \end{pmatrix}
-	      \begin{pmatrix} \vy_1 \\ \vy_2 \\ \vy_3 \end{pmatrix}
-	      &=
-	      \begin{pmatrix} c_1 \\ c_2 \\ c_3 \end{pmatrix}
-	      &
-	      \begin{pmatrix} \vy_1 \\ \vy_2 \\ \vy_3 \end{pmatrix}
-	      &\geq 
-	      0
-  \end{align*}
-  
-  \bigskip
-
-  \begin{center}
-	$
-	\begin{matrix}\mbox{\scalebox{1}{\begin{tikzpicture}
-		 \node (c1) [circle,draw] {$c_1$};
-		 \node (c2) [circle,draw,right of = c1, xshift=10mm] {$c_2$};
-		 \node (c3) [below of = c2,circle,draw,yshift=-8mm]{$c_3$};
-		 \uncover{\path[ultra thick,->] (c1) edge [] node [left] {$\vy_1$} (c3);}
-		 \uncover{\path[ultra thick,->] (c2) edge [] node [right] {$\vy_2$} (c3);}
-		 \uncover{\path[ultra thick,->] (c1) edge [] node [above]  {$\vy_3$} (c2);}
-	\end{tikzpicture}}}\end{matrix}	
-	$
-  \end{center}
-  
-\end{frame}
-
-%%%
-
-\begin{frame}{}
-\vfill
-  \begin{center}
-    \huge\bf And now?  
-  \end{center}
-  \vfill
-\end{frame}
-
-%%%
-
-\begin{frame}{A Simple Example}
-\pos{0,1.3}{
-   $
-  \begin{array}{@{}p{8mm}@{\quad}r@{\,}l@{\qquad}r@{\,}l@{\quad}r@{\,}l@{\quad}}
-    \centering $\Rot{\only<4-6>\neginfty\only<7-19>0\only<20->{42}}$
-    & \uncover<1->{\vx_1^+ &\geq \neginfty & \vx_1^+ &\geq 0 \qquad \vx_1^+ \geq \vx_3^+ + 1 } \\[0.2mm]
-    \centering $\Rot{\only<4-6>\neginfty\only<7->0}$
-    & \uncover<1->{\vx_1^- &\geq \neginfty & \vx_1^- &\geq 0   \qquad \vx_1^- \geq \vx_3^- + (-1)} \\[0.2mm]
-    \centering $\Rot{\only<4-10>\neginfty\only<11-19>0\only<20->{41}}$
-    & \uncover<1->{\vx_2^+ &\geq \neginfty & \vx_2^+ &\geq (\vx_1^- \geq -41) \;?\; \min \{ \vx_1^+, 41 \} } \\[0.2mm]
-    \centering $\Rot{\only<4-10>\neginfty\only<11->0}$
-    & \uncover<1->{\vx_2^- &\geq \neginfty & \vx_2^- &\geq  (\vx_1^- \geq -41) \;?\; \vx_1^-} \\[0.2mm]
-    \centering $\Rot{\only<4-15>\neginfty\only<16-19>0\only<20->{41}}$
-    & \uncover<1->{\vx_3^+ &\geq \neginfty & \vx_3^+ &\geq (\vx_2^- \geq -41 \;\&\; \vx_2^+ \geq 0 ) \;?\; \min \{ \vx_2^+, 41 \}} \\[0.2mm]
-    \centering $\Rot{\only<4-15>\neginfty\only<16->0}$
-    & \uncover<1->{\vx_3^- &\geq \neginfty & \vx_3^- &\geq (\vx_2^- \geq -41 \;\&\; \vx_2^+ \geq 0 ) \;?\; \min \{ \vx_2^-, 0 \} }
-  \end{array}
-  $}
-\pos{1,4.8}{\emph{Greatest Fixpoint Iteration:}}  
-\pos{1,5.4}{
-   $
-  \begin{array}{|r||p{10mm}|p{10mm}|p{10mm}|p{10mm}|p{10mm}|p{10mm}|p{10mm}|@{}l@{}}
-     & \centering 0 
-     & \centering 1
-     & \centering 2
-     & \centering 3
-     & \centering 4
-     & \centering 5
-     & \centering 6
-     & \\
-    \hline
-    \hline
-    \vx_1^+ 
-      & \centering $\infty$ 
-      & \centering $\only<3>\neginfty\only<6,9-10,13-15>0\only<18-19>\infty$
-      & \centering $\only<10,14-15>0\only<19>{42}$
-      & \centering $\only<15>0$
-      & \centering 
-      & \centering 
-      & \centering
-      &\\[0mm]\hline
-    \vx_1^- 
-      & \centering $\infty$ 
-      & \centering $\only<3>\neginfty\only<6,9-10,13-15,18-19>0$
-      & \centering $\only<10,14-15,19>0$
-      & \centering $\only<15>0$
-      & \centering 
-      & \centering 
-      & \centering
-      &\\[0mm]\hline
-    \vx_2^+ 
-      & \centering $\infty$ 
-      & \centering $\only<3,6>\neginfty\only<9-10,13-15,18-19>{41}$
-      & \centering $\only<10,14-15>0\only<19>{41}$
-      & \centering $\only<15>0$
-      & \centering 
-      & \centering 
-      & \centering
-      &\\[0mm]\hline
-    \vx_2^- 
-      & \centering $\infty$ 
-      & \centering $\only<3,6>\neginfty\only<9-10,13-15,18-19>\infty$
-      & \centering $\only<10,14-15,19>0$
-      & \centering $\only<15>0$
-      & \centering 
-      & \centering 
-      & \centering
-      &\\[0mm]\hline
-    \vx_3^+ 
-      & \centering $\infty$ 
-      & \centering $\only<3,6,9-10>\neginfty\only<13-15,18-19>{41}$
-      & \centering $\only<10>\neginfty\only<14-15,19>{41}$
-      & \centering $\only<15>0$
-      & \centering 
-      & \centering 
-      & \centering
-      &\\[0mm]\hline
-    \vx_3^- 
-      & \centering $\infty$ 
-      & \centering $\only<3,6,9-10>\neginfty\only<13-15,18-19>0$
-      & \centering $\only<10>\neginfty\only<14-15,19>0$
-      & \centering $\only<15>0$
-      & \centering 
-      & \centering 
-      & \centering
-      &\\[0mm]\hline
-  \end{array}
-  $}
-  
-  \pos{1,1.3}{\uncover<2-4>{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (2,0.5);\end{tikzpicture}}}  
-  \pos{3.4,1.3}{\uncover<5-16>{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (1.6,0.5);\end{tikzpicture}}}  
-  \pos{5.3,1.3}{\uncover<17->{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (2.5,0.5);\end{tikzpicture}}}  
-  %
-  \pos{1,1.8}{\uncover<2-4>{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (2,0.5);\end{tikzpicture}}}  
-  \pos{3.4,1.8}{\uncover<5->{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (1.6,0.5);\end{tikzpicture}}}  
-  %
-  \pos{1,2.3}{\uncover<2-7>{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (2,0.5);\end{tikzpicture}}}  
-  \pos{3.4,2.3}{\uncover<8->{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (6.0,0.5);\end{tikzpicture}}}  
-  %
-  \pos{1,2.8}{\uncover<2-7>{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (2,0.5);\end{tikzpicture}}}  
-  \pos{3.4,2.8}{\uncover<8->{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (6,0.5);\end{tikzpicture}}}  
-  %
-  \pos{1,3.3}{\uncover<2-11>{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (2,0.5);\end{tikzpicture}}}  
-  \pos{3.4,3.3}{\uncover<12->{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (7.5,0.5);\end{tikzpicture}}}  
-  %
-  \pos{1,3.8}{\uncover<2-11>{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (2,0.5);\end{tikzpicture}}}  
-  \pos{3.4,3.8}{\uncover<12->{\begin{tikzpicture}[fill opacity=0.25, opacity=0.25]\pgfsetstrokecolor{blue}\filldraw[fill=blue] (0,0) rectangle (7.5,0.5);\end{tikzpicture}}}  
-  
-  \only<21,22>{\brighten\brighten}
-
-   \only<21>{\pos{1,1}{{\bf\huge 
-     \hspace*{1.1cm}\scalebox{2}[3]{\Rot{No further}}
-     
-     \bigskip
-     \scalebox{2}[3]{\Rot{Improvement}}
-     
-     \bigskip
-     \hspace*{1.2cm}\scalebox{2}[3]{\Rot{possible!}}
-   }}}
-   \only<22>{\pos{0.3,1.5}{{\bf\huge 
-     \bigskip
-     \scalebox{2}[3.5]{\Rot{Least Solution}}
-     
-     \bigskip
-     \bigskip
-     \hspace*{3.5cm}\scalebox{2}[3.5]{\Rot{FOUND!}}
-   }}}  
-\end{frame}
-
-\frame{\frametitle{Theorem}  
-  \begin{itemize}
-    \item<2->
-      Our \emph{strategy improvement algorithm}
-      computes \emph{least solutions}. %of certain fixpoint equation systems over $\mathbb{Z} \cup \{ \neginfty, \infty \}$.
-    \bigskip
-    \item<3->
-      It can be used for performing \emph{precise zone analysis}.
-      % i.e., no widening.
-    \bigskip
-    \item<4->
-      The number of \emph{strategy improvement steps} is at most exponential.
-    \bigskip
-    \item<5->
-      Each \emph{strategy improvement step} can be carried out by \emph{ordinary greatest fixpoint iteration}.
-    \bigskip
-    \item<6->
-      The greatest fixpoint iterations can be performed in \emph{strongly polynomial time} 
-      using a reduction
-      to the \emph{minimum cost flow network problem}.
-  \end{itemize}
-}
-
-%%%
-
-\outline{3}
-
-%%%
-
-\begin{frame}{Conclusion}
-  \begin{itemize}
-    \pause\item
-      \emph{Strategy iteration} is an interesting alternative to valued-based Approaches. 
-    \pause\bigskip\item
-      Computes \emph{minimal zones} instead of some small \emph{zones}.
-    \pause\bigskip\item
-      Extensions:
-    \begin{itemize}
-        \medskip
-        \item[$\bullet$]
-          \emph{Template-based} analysis:
-          
-          \emph{Linear}:
-          \includegraphics[height=6mm]{figs/region_convex_poly}, i.e., $\vx + 2\vy \leq b_1 \wedge -\vy \leq b_2$
-          (ESOP'07)
-          
-          \emph{Quadratic}:
-          \includegraphics[height=6mm]{figs/region_convex}
-          \;
-          \includegraphics[height=6mm]{figs/region_general}, i.e., 
-            $\vx^2 + 2\vx\vy \leq b_1 \wedge \vy^2 \leq b_2$
-          (SAS'10)
-        \bigskip  
-        \item[$\bullet$]
-          Strategy Iteration + \emph{SMT solving} (ESOP'11)
-          
-          \smallskip
-          \quad From \;
-%          
-    $\begin{matrix}\text{         
-	\scalebox{0.3}{
-	\begin{tikzpicture}
-		 \node (n1) [coordinate]{};
-		 \node (n2) [coordinate,below of = n1,yshift=-10mm]{};
-		 \node (n3) [coordinate,below of = n2,yshift=-10mm]{};
-		 \path[-,ultra thick] (n1) edge [bend right] node [left,xshift=-2mm] {\huge $\mathbf{abstr.} (s_{1})$} (n2);
-		 \path[-,ultra thick] (n1) edge [bend left] node [right,xshift=2mm] {\huge $\mathbf{abstr.} (s_{1}')$} (n2);
-		 \path[->,ultra thick] (n2) edge [bend right] node [left,xshift=-2mm] {\huge $\mathbf{abstr.} (s_{2})$} (n3);
-		 \path[->,ultra thick] (n2) edge [bend left] node [right,xshift=2mm] {\huge $\mathbf{abstr.} (s_{2}')$} (n3);
-	\end{tikzpicture}
-	}}\end{matrix}$
-%
-        \;  to \;
-% 
-    $\mathbf{abstr.} \begin{pmatrix}\text{         
-	\scalebox{0.3}{
-	\begin{tikzpicture}
-		 \node (n1) [coordinate]{};
-		 \node (n2) [coordinate,below of = n1,yshift=-10mm]{};
-		 \node (n3) [coordinate,below of = n2,yshift=-10mm]{};
-		 \path[-,ultra thick] (n1) edge [bend right] node [left,xshift=-2mm] {\huge $s_{1}$} (n2);
-		 \path[-,ultra thick] (n1) edge [bend left] node [right,xshift=2mm] {\huge $s_{1}'$} (n2);
-		 \path[->,ultra thick] (n2) edge [bend right] node [left,xshift=-2mm] {\huge $s_{2}$} (n3);
-		 \path[->,ultra thick] (n2) edge [bend left] node [right,xshift=2mm] {\huge $s_{2}'$} (n3);
-	\end{tikzpicture}
-	}}\end{pmatrix}$
-%
-      
-      \medskip\item[$\bullet$]
-          \emph{Unbounded Time} Verification 
-          for \emph{Cyber-Physical Systems}
-          through Abstract Interpretation (ATVA'11, APLAS'11, Current Work)
-    \end{itemize}
-  \end{itemize}  
-
-  \vspace*{-2mm}
-  \begin{center}
-    \Large\bf
-    \pause Thanks for Your Attention! \pause Questions?
-  \end{center}
-\end{frame}
-
-%%%
-
-\begin{frame}[allowframebreaks]{References}
-  \bibliographystyle{apalike2}
-  \bibliography{bib}  
-\end{frame}