diff options
Diffstat (limited to 'tex/presentation/thomas/slides.tex')
| -rw-r--r-- | tex/presentation/thomas/slides.tex | 780 |
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} |