\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}