From 2ee29b3426d2d79872fba35adbeb8d768983ffec Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro 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