Delete a lot of tex stuff, better debug info

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

1 files changed, 0 insertions, 290 deletions

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}