From 2ee29b3426d2d79872fba35adbeb8d768983ffec Mon Sep 17 00:00:00 2001
From: Carlo Zancanaro <carlo@carlo-laptop>
Date: Thu, 19 Apr 2012 16:21:26 +1000
Subject: Add presentation; start a different implementation

---
 tex/presentation/slides.tex | 655 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 655 insertions(+)
 create mode 100644 tex/presentation/slides.tex

(limited to 'tex/presentation/slides.tex')

diff --git a/tex/presentation/slides.tex b/tex/presentation/slides.tex
new file mode 100644
index 0000000..dbb76f0
--- /dev/null
+++ b/tex/presentation/slides.tex
@@ -0,0 +1,655 @@
+\documentclass{beamer}
+
+\usepackage{amsmath,graphicx,makeidx,listings,colortbl,helvet,ifthen,tikz,pgfpages,ifthen}
+
+\begin{document}
+
+\begin{frame}{Abstract Domain: {\bf Zones} (1/2)}
+      \bf Goal: \emph{Tight bounds} on the possible values of \emph{integer variables}
+      
+      \qquad\qquad (like $x_1 \leq 42, \; x_2 \leq 13$)
+
+      \bigskip
+      \qquad$\leadsto$ buffer overflows, worst-case execution times, etc.
+      
+      \bigskip
+      \bf Definition:
+      Invariants of the form 
+      \begin{align*}
+        \bigwedge_x x \leq b_{x} \wedge \bigwedge_x -x \leq b_{-x} \wedge \bigwedge_{x,y} x - y \leq b_{x-y}
+      \end{align*}
+      That is:
+               \emph{bounds} on \emph{variables} and
+                \emph{differences of variables}.
+
+      \bigskip
+      \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)}
+    \bf Our point of view:
+    Zones are special \emph{template polyhedra}
+    
+    \smallskip
+    \qquad$\leadsto$ template polyhedra: \cite{DBLP:conf/vmcai/SankaranarayananSM05}
+ 
+    \bigskip
+    \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*}	
+
+  \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\{
+  \bf Goal: 
+  Find minimal \emph{zones} that are \emph{invariants}
+ 
+  \bigskip
+  \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}
+
+  \vspace*{-5mm}
+  For program point $a$:
+
+  \smallskip
+  $
+    \gamma \left( 
+      \begin{pmatrix} \infty \\ \infty \\ \infty \end{pmatrix} 
+    \right)
+    =
+    \left\{ 
+      \begin{pmatrix} x_1\\x_2 \end{pmatrix} 
+      \mid
+	      \begin{pmatrix}
+	        1 & 0 \\
+	        0 & 1 \\
+	        -1 & 1
+	      \end{pmatrix}
+      \begin{pmatrix} x_1\\x_2 \end{pmatrix} 
+      \leq 
+      \begin{pmatrix} \infty \\ \infty \\ \infty \end{pmatrix}            
+    \right\}
+  $
+
+  \bigskip
+  For program point $b$:
+
+  \smallskip
+  $
+    \gamma \left( 
+      \begin{pmatrix} 10 \\ 11 \\ 1 \end{pmatrix} 
+    \right)
+    =
+    \left\{ 
+      \begin{pmatrix} x_1\\x_2 \end{pmatrix} 
+      \mid
+	      \begin{pmatrix}
+	        1 & 0 \\
+	        0 & 1 \\
+	        -1 & 1
+	      \end{pmatrix}
+      \begin{pmatrix} x_1\\x_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
+    \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 $x = x + d$ and $x = y + 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
+    \emph{Properties}:
+    \begin{itemize}
+      \smallskip\item<9->
+         Computed the \emph{minimal} zones that are invariant
+      \smallskip\item<10->
+         Arbitrary affine assignments (like $x = c_1 x_1 + \cdots + c_k x_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
+    Can we do better?
+  \end{center}
+
+  \begin{center}  
+  \bigskip
+  \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}
+
+  \bigskip
+  \bigskip
+  \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}
+      \emph{Statements} %
+      %
+      \begin{align*}
+        T x \leq c \; \wedge \;  x' = A x + d
+      \end{align*}
+
+      \emph{Collecting Semantics} %
+      %
+      \begin{align*}
+        \sem{T x \leq c \; \wedge \;  x' = A x + d} (X) 
+        =
+        \{ x' \mid x \in X \wedge Tx \leq c \wedge x' = Ax+d \} 
+      \end{align*}
+
+      \emph{Abstract Semantics} %
+      %
+      \begin{align*}
+        \sem{T x \leq c \; \wedge \;  x' = A x + d}^\sharp (b)
+          &= \alpha(\sem{T x \leq c \; \wedge \;  x' = A x + 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$};
+		 \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
+	T 
+	=
+	      \begin{pmatrix}
+	        1 & 0 \\
+	        0 & 1 \\
+	        -1 & 1
+	      \end{pmatrix}
+	$
+  }
+
+  \pos{0.3,4}{\bf Least Solution of}
+  
+  \pos{0.3,4.5}{
+  $
+    \begin{array}{@{}r@{}l}
+    {\vb^a_{1} &\geq \infty \\}
+    {\vb^a_{2} &\geq \infty \\}
+    {\vb^a_{3} &\geq \infty}
+    \\[5pt]
+    {\vb^b_{1} &\geq \pi_{1}(\sem{\stmtone}^\sharp (\vb^a_{1}, \vb^a_{2}, \vb^a_{3})) \\}
+    {\vb^b_{2} &\geq \pi_{2}(\sem{\stmtone}^\sharp (\vb^a_{1}, \vb^a_{2}, \vb^a_{3})) \\}
+    {\vb^b_{3} &\geq \pi_{3}(\sem{\stmtone}^\sharp (\vb^a_{1}, \vb^a_{2}, \vb^a_{3}))}
+    \\[5pt]
+    {\vb^b_{1} &\geq \pi_{1}(\sem{\stmttwo}^\sharp (\vb^b_{1}, \vb^b_{2}, \vb^b_{3})) \\}
+    {\vb^b_{2} &\geq \pi_{2}(\sem{\stmttwo}^\sharp (\vb^b_{1}, \vb^b_{2}, \vb^b_{3})) \\}
+    {\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}
+  \bf Observation:
+  %
+  \only<1-10>{%
+      \begin{align*}
+         &\pi_{k}(\sem{T x \leq c \; \wedge \;  x' = A x + d}^\sharp (b)) \\
+         {=\;& \pi_{k}( \alpha(\sem{T x \leq c \; \wedge \;  x' = A x + d} (\gamma( b ))) ) \\}
+         {=\;& \pi_{k}( \alpha(\sem{T x \leq c \; \wedge \;  x' = A x + d} ( \{ x \in \Z^n \mid Tx \leq b \} )) ) \\}
+         {=\;& \pi_{k}( \alpha( \{ x' \mid x, x' \in \Z^n \;\wedge\; T x \leq b, c \; \wedge \;  x' = A x + d \} ) ) \\}
+         {=\;& \pi_{k}( \alpha( \{ A x + d \mid x \in \Z^n \;\wedge\; T x \leq \min(b, c)  \} ) ) \\}
+         {=\;& \sup \; \{ T_k(A x + d) \mid x \in \Z^n \;\wedge\; T x \leq \min(b, c)  \} \\}
+         {=\;& T_k d + \sup \; \{ T_k A x \mid x \in \Z^n \;\wedge\;  T x \leq \min ( b, c )  \}  \\}
+         {=\;& T_k d + \sup \; \{ T_k A x \mid x \in \R^n \;\wedge\;  T x \leq \min ( b, c )  \}  \\}
+         {=\;& T_k d + \inf \; \{ (\min( b, c ))^\top y \mid y \in \R_{\geq 0}^n \wedge T^\top y = (T_1A)^\top y  \}  \\}
+         {=\;& T_k d + \inf \; \{ (\min( b, c ))^\top y \mid y \in \Z_{\geq 0}^n \wedge T^\top y = (T_1A)^\top y  \}  \\}
+      \end{align*}%
+  }%
+  \only<11->{%
+      \begin{align*}
+         &\pi_{k}(\sem{T x \leq c \; \wedge \;  x' = A x + d}^\sharp (b)) \\
+         {=\;& T_k d + \inf \; \{ (\min( b, c ))^\top y \mid y \in \Z_{\geq 0}^n \wedge T^\top y = (T_1A)^\top y  \}  \\}
+      \end{align*}
+  }%
+      
+   {
+      \bf Consequences:
+      
+      \bigskip
+      $\pi_k \circ \sem{T x \leq c \; \wedge \;  x' = A x + 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
+%      \bf So What?
+%    }
+\end{frame}
+
+%%%
+
+\begin{frame}{Minimum Cost Flow Network Problem}
+  \begin{align*}
+    \min  \;\; b^\top \begin{pmatrix} y_1 \\ y_2 \\ y_3 \end{pmatrix} 
+    \qquad\qquad
+    \\[10pt]
+    %
+	      \begin{pmatrix}
+	        1 & 0 & -1 \\
+	        0 & 1 & 1\\
+	        -1 & -1 & 0
+	      \end{pmatrix}
+	      \begin{pmatrix} y_1 \\ y_2 \\ y_3 \end{pmatrix}
+	      &=
+	      \begin{pmatrix} c_1 \\ c_2 \\ c_3 \end{pmatrix}
+	      &
+	      \begin{pmatrix} y_1 \\ y_2 \\ y_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] {$y_1$} (c3);}
+		 \uncover{\path[ultra thick,->] (c2) edge [] node [right] {$y_2$} (c3);}
+		 \uncover{\path[ultra thick,->] (c1) edge [] node [above]  {$y_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}}$
+    & {x_1^+ &\geq \neginfty & x_1^+ &\geq 0 \qquad x_1^+ \geq x_3^+ + 1 } \\[0.2mm]
+    \centering $\Rot{\only<4-6>\neginfty\only<7->0}$
+    & {x_1^- &\geq \neginfty & x_1^- &\geq 0   \qquad x_1^- \geq x_3^- + (-1)} \\[0.2mm]
+    \centering $\Rot{\only<4-10>\neginfty\only<11-19>0\only<20->{41}}$
+    & {x_2^+ &\geq \neginfty & x_2^+ &\geq (x_1^- \geq -41) \;?\; \min \{ x_1^+, 41 \} } \\[0.2mm]
+    \centering $\Rot{\only<4-10>\neginfty\only<11->0}$
+    & {x_2^- &\geq \neginfty & x_2^- &\geq  (x_1^- \geq -41) \;?\; x_1^-} \\[0.2mm]
+    \centering $\Rot{\only<4-15>\neginfty\only<16-19>0\only<20->{41}}$
+    & {x_3^+ &\geq \neginfty & x_3^+ &\geq (x_2^- \geq -41 \;\&\; x_2^+ \geq 0 ) \;?\; \min \{ x_2^+, 41 \}} \\[0.2mm]
+    \centering $\Rot{\only<4-15>\neginfty\only<16->0}$
+    & {x_3^- &\geq \neginfty & x_3^- &\geq (x_2^- \geq -41 \;\&\; x_2^+ \geq 0 ) \;?\; \min \{ x_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
+    x_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
+    x_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
+    x_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
+    x_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
+    x_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
+    x_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}{{\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}{{\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}{{\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}{{\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}{{\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}{{\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., $x + 2y \leq b_1 \wedge -y \leq b_2$
+          (ESOP'07)
+          
+          \emph{Quadratic}:
+          \includegraphics[height=6mm]{figs/region_convex}
+          \;
+          \includegraphics[height=6mm]{figs/region_general}, i.e., 
+            $x^2 + 2xy \leq b_1 \wedge y^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}
+\end{document}
-- 
cgit v1.2.3

