From 608cf2e6a2ccc967e82b2b7a9693fd0bafb778fb Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Wed, 5 Sep 2012 10:25:19 +1000 Subject: Delete a lot of tex stuff, better debug info Some other stuff, too, I think. Oh well. No biggie! --- tex/presentation/main.tex | 290 ---------------------------------------------- 1 file changed, 290 deletions(-) delete mode 100644 tex/presentation/main.tex (limited to 'tex/presentation/main.tex') diff --git a/tex/presentation/main.tex b/tex/presentation/main.tex deleted file mode 100644 index 286e4a7..0000000 --- a/tex/presentation/main.tex +++ /dev/null @@ -1,290 +0,0 @@ -\documentclass{beamer} - -\usetheme{Hannover} -\usepackage{amsmath,stmaryrd,listings} - -\title{{\bf Static Analysis \\ through \\Abstract Interpretation, \\Convex Optimization, and\\ Strategy Iteration}} - -\author{ - {\bf Thomas Martin Gawlitza} - \\[3pt] - joint work with - \\[3pt] - {\bf Helmut Seidl} -} - -\newcommand\N{\mathbb{N}} -\newcommand\Z{\mathbb{Z}} -\newcommand\CZ{\overline{\Z}} - -\let\max\undefined -\newcommand\max{\lor} -\let\min\undefined -\newcommand\min{\land} - -\begin{document} - -\begin{frame} - \maketitle -\end{frame} - -\begin{frame} - \tableofcontents -\end{frame} - -\section{Example} -\begin{frame}{Example} - \begin{eqnarray*} - x_1 &=& 0 \max (-1 + x_1 \min x_2) \\ - x_2 &=& 0 \max 5 + x_1 \max x_1 \\ - x_3 &=& 0 \max 1 + x_3 \max 0 + x_1 - \end{eqnarray*} - -\end{frame} - -\section{Definitions} -\begin{frame}{Preliminary Definitions} - \begin{center} - Strange notation: \\ - $x \max y = \text{max}(x, y)$ \\ - $x \min y = \text{min}(x, y)$ \\ - \uncover<2->{ - \bigskip - {\bf Monotone:} $x \leq y \implies f(x) \leq f(y) ~~ \forall x,y$ - } - - \uncover<3->{ - \bigskip - {\bf Assignment:} $\rho$ is always a variable assignment (from $X \rightarrow \CZ$) - } - \end{center} -\end{frame} - -\begin{frame}{Systems of Equations} - \begin{align*} - \varepsilon = \{ x_1 = e_1, x_2 = e_2, ... x_n = e_n \} - \end{align*} - \uncover<2->{ - \begin{align*} - \text{\bf Solutions: } & \rho = \llbracket \varepsilon \rrbracket \rho \\ - \text{\bf Presolutions: } & \rho \leq \llbracket \varepsilon \rrbracket \rho \\ - \text{\bf Fixpoint: } & f(x) = x \\ - \text{\bf Least fixpoint: } & \mu f \\ - \end{align*} - } - \uncover<3->{ - {\bf Evaluation:} - $\text{with } \rho ~ \epsilon ~ Vars(\varepsilon) \rightarrow \CZ$ \\ - \begin{align*} - (\llbracket \varepsilon \rrbracket \rho)(x) & := \llbracket e \rrbracket \rho \\ - \llbracket x \rrbracket \rho & := \rho (x) \\ - \llbracket f(e_1, ... e_k) \rrbracket & := f(\llbracket e_1 \rrbracket \rho, - ... \llbracket e_k \rrbracket \rho) - \end{align*} - } -\end{frame} - -\begin{frame}{Operators on $\CZ$} - Working in $\CZ = \Z \cup \{\infty, -\infty\}$ - - \bigskip - \begin{displaymath} - x +^{-\infty} y = \left\{ \begin{array}{ll} - -\infty & \text{if } -\infty \in \{x,y\} \\ - \infty & \text{if } -\infty \not\in \{x,y\} \text{ and } \infty \in \{x,y\} \\ - x + y & \text{if } x,y \in \Z \\ - \end{array} \right. - \end{displaymath} - \begin{displaymath} - x +^{\infty} y = \left\{ \begin{array}{ll} - \infty & \text{if } \infty \in \{x,y\} \\ - -\infty & \text{if } \infty \not\in \{x,y\} \text{ and } -\infty \in \{x,y\} \\ - x + y & \text{if } x,y \in \Z \\ - \end{array} \right. - \end{displaymath} - \begin{displaymath} - \begin{array}{lr} - x \cdot \infty = \infty \cdot x = \infty, - x \cdot -\infty = -\infty \cdot x = -\infty - & \forall x > 0 \\ - x \cdot \infty = \infty \cdot x = -\infty, - x \cdot -\infty = -\infty \cdot x = \infty - & \forall x < 0 \\ - 0 \cdot \infty = \infty \cdot 0 = - 0 \cdot -\infty = -\infty \cdot 0 = 0 & - \end{array} - \end{displaymath} -\end{frame} - -\begin{frame}{Expansivity} - $f$ is upward-expansive in $X'$ iff - - \bigskip - \begin{center} - $f(\rho \oplus \{x \mapsto \rho(x) + \delta\}) \geq f(\rho) + \delta)$ - ~~ $\forall x \in X', \rho \in X \rightarrow \CZ, \delta \in \N$ - \end{center} -\end{frame} - -\section{Max-strategies} -\begin{frame}{Max-strategies} - Assume for every $x = e \in \varepsilon$, $e$ is of the - form $e_1 \max e_2 \max ... \max e_k$. - - Then a $\max$-$strategy$ $\sigma$ maps each $e$ to one of its $e_k$. - - \bigskip - For all $\max$ strategies $\sigma$ the expression $e\sigma$ is defined as: - \begin{align*} - (e_1 \max ... \max e_k)\sigma & = (\sigma(e_1 \max ... \max e_k))\sigma \\ - (f(e_1,...e_k))\sigma & = f(e_1\sigma, ..., e_k\sigma) - \end{align*} - where $f \not = \max$ -\end{frame} - -\begin{frame}{Max-strategies} - We may need to change strategy throughout our evaluation. - - Consider the system: $\varepsilon = \{x_1 = x_1 + 1 \max 0\}$. - - Let: - \begin{align*} - \sigma_1 & = \{x_1 + 1 \max 0 \mapsto x_1 + 1\} \\ - \sigma_2 & = \{x_1 + 1 \max 0 \mapsto 0\} - \end{align*} - - \uncover<2->{ - This gives us: - } - \begin{align*} - \uncover<2->{ - \mu \llbracket \varepsilon (\sigma_1) \rrbracket & = \{x_1 \mapsto -\infty\} \\ - \mu \llbracket \varepsilon (\sigma_2) \rrbracket & = \{x_1 \mapsto 0\} \\ - } - \uncover<3->{ - \mu \llbracket \varepsilon \rrbracket & = \{x_1 \mapsto \infty\} - } - \end{align*} -\end{frame} - -\section{Bellman-Ford} -\begin{frame}{BF-functions} - $X$ a set. A monotone $f: (X \rightarrow \CZ) \rightarrow CZ$ is called - a \emph{Bellman-Ford function} iff, $\forall \rho, \rho': X \rightarrow \CZ$ - with $\rho' \geq \rho$ the following holds: - - \bigskip - If $f(\rho') > f(\rho)$ then $\exists x \in X$ and some $\delta \in \CZ\setminus\{-\infty\}$ such that: - \begin{align*} - \rho'(x) & > \rho(x) \\ - f(\rho') & = \rho'(x) + \delta \\ - f(\rho'') & \geq \rho''(x) + \delta ~~ \forall \rho'' \geq \rho' - \end{align*} -\end{frame} - -\begin{frame}{A quick lemma} - Let $\varepsilon$ be a system of \emph{BF-equations} with $n$ variables. \\ - Let $\rho^{(i)} = \llbracket\varepsilon\rrbracket^i(\_ \mapsto -\infty) ~~ \forall i \in \N$. \\ - The following holds for every $x \in Vars(\varepsilon)$: \\ - If there exists some $k > n$ with $\rho^{(k)}(x) > \rho^{(n)}(x)$, then - $\mu\llbracket\varepsilon\rrbracket(x) = \infty$. -\end{frame} - -\begin{frame}{The algorithm} - ~ \\ - {\bf Input:} A system of BF-equations with $n$ variables \\ - {\bf Output:} The least solution $\mu\llbracket\varepsilon\rrbracket$ of \varepsilon \\ - \begin{displaymath} - ~ \\ - \rho \leftarrow (\_ \mapsto -\infty) \\ - {\bf for} i = 1 {\bf to} n {\bf do} \rho \leftarrow \llbracket\varepsilon\rrbracket\rho \\ - \rho \leftarrow \rho' \text{ where } \rho'(x) = \left\{ \begin{array}{ll} - \rho(x) & \text{if } (\llbracket\varepsilon\rrbracket\rho)(x) \leq \rho(x) \\ - \infty & \text{if } (\llbracket\varepsilon\rrbracket\rho)(x) > \rho(x) - \end{array} \right. \forall x \in X \\ - {\bf for} i = 1 {\bf to} n-1 {\bf do} \rho \leftarrow \rho \max \llbracket\varepsilon\rrbracket\rho \\ - {\bf return} \rho \\ - ~ - \end{displaymath} -\end{frame} - -\begin{frame}{Example} - \begin{align*} - x & = 1 \\ - y & = y + x \max -10 \\ - z & = x \cdot^+ y - \end{align*} - Where $\cdot^+$ is defined by: - \begin{displaymath} - x \cdot^+ y = \left\{ \begin{array}{l l} - x \cdot y & \text{if } x, y > 0 \\ - -\infty & \text{if } x \le 0 \text{ or } y \le 0 - \end{array} \forall x,y \in \CZ - \end{displaymath} -\end{frame} - -\section{Max-strategy improvement} -\begin{frame}{Max-strategy improvement} - {\bf General idea:} - \begin{itemize} - \item Pick a max-strategy - \item Perform fixpoint iteration - \item Improve strategy - \item Repeat until we have a solution - \end{itemize} -\end{frame} - -\begin{frame}{What is an improvement?} - If we have $\varepsilon$ a system of equations, $\sigma$ a $\max$-strategy - for $\varepsilon$ and $\rho$ a presolution of $\varepsilon(\sigma)$, then we - call a $\max$-strategy $\sigma'$ is called an improvement of $\sigma$ with - respect to $\rho$ iff: - \begin{itemize} - \item if $\rho \not \in {\bf Sol}(\varepsilon)$, then $\llbracket\varepsilon(\sigma')\rrbracket\rho > \rho$ - \item for all $\max$-expression $e \in S_{\max}(\varepsilon)$ the following holds: \\ - If $\sigma'(e) \not = \sigma(e)$, then $\llbracket e\sigma'\rrbracket\rho > \llbracket e\sigma\rrbracket\rho$ - \end{itemize} -\end{frame} - -\begin{frame}{Algorithm} - ~ \\ - {\bf Input:} - \begin{itemize} - \item A system $\varepsilon$ of monotone equations over a complete linearly ordered set \\ - \item A $\max$-strategy $\sigma_{init}$ for $\varepsilon$ \\ - \item A pre-solution $\rho_{init}$ of $\varepsilon(\sigma_{init})$ with $\rho_{init} \le \mu\llbracket\varepsilon\rrbracket$ - \end{itemize} - {\bf Output:} The least solution $\mu\llbracket\varepsilon\rrbracket$ of $\varepsilon$ - \begin{displaymath} - ~ \\ - \sigma \leftarrow \sigma_{init} \\ - \rho \leftarrow \rho_{init} \\ - \text{while }(\rho \not \in {\bf Sol}(\varepsilon)) \{ \\ - ~~~~ \sigma \leftarrow P_{\max}(\sigma, \rho) \\ - ~~~~ \rho \leftarrow \mu_{\ge\rho} \llbracket\varepsilon(\sigma)\rrbracket \\ - \} \\ - {\bf return} \rho - ~ - \end{displaymath} -\end{frame} - -\begin{frame}{Another related lemma} - Whenever the $\max$-strategy improvement algorithm terminates, it - returns the least solution $\mu\llbracket\varepsilon\rrbracket$. -\end{frame} - -\begin{frame}{Example} - \begin{align*} - x_1 & = 0 \max x_1 + x_2 - 4 \\ - x_2 & = -1 \max ((x_1 + 1 \max 2 \cdot x_2) \min 5) - \end{align*} -\end{frame} - -\section{Feasibility} - -\section{Extended Integer Equations} - -\section{Abstract Interpretation over Zones} - - -\end{document} -- cgit v1.2.3