\documentclass[12pt]{beamer}
\usetheme{Boadilla}

\title{Abstract interpretation}
\author{David Monniaux}
\institute{CNRS / VERIMAG}
\date{May 23--27, Menlo College}

\graphicspath{{../logos/}{../pics/}{pics/}}
\logo{\includegraphics[height=7mm]{logo_VERIMAG_vectorise}
\includegraphics[height=7mm]{WEB_CNRS-filaire-Quadri}}

\usepackage{tikz}
\usetikzlibrary{arrows,automata}
\tikzstyle{block} = [rectangle, inner sep=1ex, draw]
\tikzstyle{loopblock} = [block, line width=1.5pt]
\tikzstyle{edge} = [draw,->]

\usepackage{verbatim,listings}
\lstset{language=C++,basicstyle={\rm\fontfamily{ppl}\selectfont},mathescape=true,morekeywords={assume,assert}}

\AtBeginSection[]{\begin{frame}<beamer>
\tableofcontents[currentsection]
\end{frame}}

\AtBeginSubsection[]
{
    \begin{frame}{Outline}
        \tableofcontents[currentsection,currentsubsection]
    \end{frame}
}

\newcommand{\stress}[1]{\textbf{\textcolor{red}{#1}}}

% \newcommand{\finger}{\ding{43}~}
\newcommand{\finger}{$\Rightarrow$}

\usepackage{amssymb,amsfonts}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\abstr}[1]{#1^\sharp}
\newcommand{\post}{\text{post}}
\newcommand{\lfp}{\mathop{\text{lfp}}}

\begin{document}
\begin{frame}
\maketitle
\end{frame}

\begin{frame}{Grenoble}
\begin{center}
\includegraphics[height=7.5cm]{Grenoble_in_France}
\end{center}
\end{frame}

\begin{frame}{Grenoble}
\begin{center}
\includegraphics[height=6cm]{Grenoble_from_Moucherotte_IMG_0861_tuned_shrunk}
\end{center}
\end{frame}

\begin{frame}{VERIMAG}
\begin{center}
\includegraphics[height=5cm]{VERIMAG_P1160419_constrast_shrunk}
\end{center}

Joint lab between CNRS and Grenoble University

9 CNRS permanent researchers + 4 research engineers

23 professors
\end{frame}
% DR
% Halbwachs
% Maler
% Sifakis
% Graf
% CR1
% Monniaux
% Raymond
% Dang
% Iosif
% CR2
% Jobstmann

\section{Introduction}

\subsection{Position within other techniques}
\begin{frame}{Static analysis}

Establish automatically that a \stress{program} meets a \stress{specification}.
\bigskip

Specification can be:
\begin{enumerate}
\item Explicit, e.g. ``the program sorts the integer array given as input''.
\smallskip

Can be expressed by e.g. temporal logics, assertions\dots
\medskip

\item Implicit, e.g. ``the program never crashes due to division by zero, array overflow, bad pointer dereference''.
\smallskip

Easier for the programmer (no need to write anything in addition to the code).
\end{enumerate}
\end{frame}

\begin{frame}{Impossibilities}

Turing's Halting Problem / Rice's Theorem
\bigskip

Program analysis is impossible unless one condition is met:
\begin{enumerate}
\item Not fully automatic, requires user interaction.
\item Constrained enough class of programs.
\item Finite memory.
\item Finite number of program steps.
\item Analysis can answer \stress{false positives}.
\item Analysis can answer \stress{false negatives}.
\end{enumerate}
\end{frame}

\begin{frame}{User interaction}

Example: \stress{interactive theorem proving}.
\bigskip

Program analysis problems generally map to logics (e.g. Peano arithmetic)
with no decision procedure.
\medskip

(Actually a way to prove undecidability of such logics\dots)
\end{frame}

\begin{frame}{Finite memory}

Can enumerate \stress{reachable states} explicitly.
\bigskip

\stress{Computable} but costly: $n$ bits of memory in analyzed system

\finger $2^n$ states in analyzer
\end{frame}

\begin{frame}{Finite number of program steps}

Finite number of program steps

+ program statements with semantics in logics
e.g. linear arithmetic

\finger

\stress{Bounded model checking}.
\end{frame}

\begin{frame}{Analysis can produce false negatives}

\stress{False negative} = some bugs may be ignored
\bigskip

Examples of techniques:
\begin{itemize}
\item \stress{testing}
\item \href{http://www.coverity.com/}{Coverity}
\end{itemize}
\end{frame}

\begin{frame}{(Semantically sound) static analysis}

Deducing \stress{properties} of software
\begin{itemize}
\item From a mathematical model of its behaviour (\stress{semantics}).
\item Examples: ``no division by zero'', ``no assertion failure''
\item valid for \stress{all executions}
\item using safe \stress{over-approximation} of behaviors
\begin{itemize}
\item \stress{no false negatives}
\item maybe false positives (\stress{false alarms})
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{A central problem}

{\Large \stress{Higher precision (fewer false alarms)\\
vs scaling-up (low higher time/space costs)}}
\bigskip

Want to have them both?
\end{frame}

\subsection{A short chronology}

\begin{frame}{Ariane V, maiden flight, 1996}

\begin{center}
\includegraphics[height=7cm]{Ariane_60}
\end{center}
\end{frame}

\begin{frame}{Ariane V self-destructing}
\begin{center}
\includegraphics[height=7cm]{Ariane_138}
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{Arithmetic overflow}

\begin{minipage}{3cm}
\includegraphics[width=4cm]{Ariane_138}
\end{minipage}
\hfill
\begin{minipage}{7cm}
\begin{lstlisting}
x = computation_for_Ariane4();
y = (short int) x;
\end{lstlisting}

{\footnotesize (ok it was Ada, not C)}
\bigskip

\pause
\textcolor{violet}{\finger PolySpace Verifier (1996--)}\\(Deutsch et al.; commercial tool)
\bigskip

Bug found by \stress{direct automated analysis of the source code}.
\end{minipage}
\end{frame}

\begin{frame}{A modern airplane: Airbus A380}

\includegraphics[width=5.7cm]{Airbus_A380_P1230288_shrunk}
\hfill
\includegraphics[width=5.7cm]{Airbus_A380_cockpit_joystick}
\bigskip

\pause
\textcolor{violet}{\finger Astr\'ee (2002--)} (Cousot et al.)
\bigskip

Prove \stress{absence of bugs}.
\bigskip

I was a key member of Astr\'ee (now sold commercially).
\end{frame}

\begin{frame}{Safety-critical embedded systems}

\begin{itemize}
\item Airplanes (DO-178C), trains, space launchers
\item Nuclear plants, electrical grid controls
\item Medical devices
\end{itemize}
\bigskip

US Food and Drug Administration, action on \stress{infusion pumps} (2010).
\begin{center}
\includegraphics[height=4cm]{infusion_pump}
\end{center}
\end{frame}

\begin{frame}{At Microsoft\dots}

Microsoft Device Driver Verifier (from project SLAM)
\medskip

CodeContracts
\medskip

etc.
\end{frame}

\subsection{Basic ideas}

\begin{frame}{Large state spaces}

We cannot represent the \stress{concrete state space}~$X$.

Four 32-bit variables: $2^{128}$ states.

Too large for explicit-state model-checking (need to memorize all states in memory)\dots

and also for implicit-state model-checking (using clever structures e.g. BDDs)
\end{frame}

\begin{frame}{Solution}

Instead of a set of states $s \subseteq X$ use another $\abstr{s}$ simpler to represent.
\bigskip

e.g. with $X = \ZZ^2$, $s \subseteq X$ a set of pairs of integers,
$\abstr{s}$ a product of 2 intervals
\bigskip

\stress{We do not forget behaviors}: since $s \subseteq \abstr{s}$, cannot
forget any reachable state.
\end{frame}

\section{Transition systems}

\begin{frame}{Initial states + transitions}

Program or machine state = values of variables, registers, memories\dots
within state space $\Sigma$.
\bigskip

Examples:
\begin{itemize}
\item if system state = 17-bit value, then $\Sigma = \{ 0, 1\}^{17}$\,;
\item = 3 unbounded integers, $\Sigma = \ZZ^3$\,;
\item if finite automaton, $\Sigma$ is the set of states\,;
\item if stack automaton, complete state = couple (finite state, stack contents), thus $\Sigma = \Sigma_S \times \Sigma_P ^*$.
\end{itemize}
\bigskip

\stress{Transition relation} $\rightarrow$~ $x \rightarrow y$ = ``if at $x$ then can go to $y$ at next time''
\end{frame}

\begin{frame}{Safety properties}

Show that a program does not reach an \stress{undesirable state} (crash, error, out of specification). Set $W$ of undesirable states.
\bigskip

Show that there is no $n \geq 0$ and
$\sigma_0 \rightarrow \sigma_1 \rightarrow \dots \sigma_n$
s.t. $\sigma_0$ initial state (= reset) and $\sigma_n \in W$
\bigskip

Otherwise said $\sigma_0 \rightarrow^* \sigma_n \in W$. $\rightarrow^*$ \stress{transitive closure} of $\rightarrow$.
\end{frame}

\begin{frame}{Reachable states}

$\Sigma_0 \subseteq \Sigma$ set of initial states. \stress{Reachable states} $A$ set of states $\sigma$ s.t.
\begin{equation}
\exists \sigma_0 \in \Sigma_0~ \sigma_0 \rightarrow^* \sigma
\end{equation}
\bigskip

Goal: show that $A \cap W = \emptyset$.
\end{frame}


\begin{frame}{Computation}

$X_n$ set of states reachable in at most $n$ turns of~$\rightarrow$:
$X_0 = \Sigma_0$, $X_1 = \Sigma_0 \cup R(\Sigma_0)$, $X_2 = \Sigma_0 \cup R(\Sigma_0) \cup R(R(\Sigma_0))$, etc.
\medskip

with $R(X) = \{ y \in \Sigma \mid \exists x \in X ~ x \rightarrow y \}$.
\bigskip

The sequence $X_k$ is ascending for~$\subseteq$.
Its limit (= the union of all iterates) is the \stress{set of reachable states}.
\end{frame}

\begin{frame}{Iterative computation}

Remark $X_{n+1} = \phi(X_n)$ with $\phi(X) = \Sigma_0 \cup R(X)$.
\bigskip

Intuition: to reach in at most $n+1$ turns
\begin{itemize}
\item either in 0 turns, thus on an initial state: $\Sigma_0$
\item either in $0 < k \leq n+1$ coups, otherwise said at most $n$ turns ($X_n$), then another turn.
\end{itemize}
\bigskip

How to \stress{compute efficiently} the $X_n$? And the limit?
\end{frame}

\begin{frame}{Explicit-state model-checking}

Explicit representations of $X_n$ (list all states).\bigskip

If $\Sigma$ finite, $X_n$ converges in at most $|\Sigma|$ iterations.
\medskip

Reason:
\begin{itemize}
\item Either $X_n = X_{n+1}$, thus remains constant.
\item Either $X_n \subsetneq X_{n+1}$, then $X_{n+1} \setminus X_n$ contains at least 1 state. Cannot happen more than $|\Sigma|$ times.
\end{itemize}
\end{frame}

\begin{frame}{Inductive invariants}

(Inductive) invariant: set $X$ of states s.t. $\phi(X) \subseteq X$.
Recall
\begin{equation}
\phi(X) = X_0 \cup \{ y \in \Sigma \mid \exists x \in X ~ x \rightarrow y \}
\end{equation}
\bigskip

If $X$ et $Y$ two invariants, then so is $X \cap Y$.
\bigskip

$\phi$ \stress{monotonic} for $\subseteq$ (if $X \subseteq Y$, then $\phi(X) \subseteq \phi(Y)$).
\bigskip

$\phi(X \cap Y) \subseteq \phi(X) \subseteq X$, same for $Y$, thus $\phi(X \cap Y) \subseteq X \cap Y$.
\bigskip

Same for intersections of infinitely many invariants.
\end{frame}

\begin{frame}{The strongest invariant}

Intersect all invariants, obtain \stress{least invariant} / \stress{strongest invariant}.
\bigskip

This invariant satisfies $\phi(X) = X$, it is the \stress{least fixed point} of $\phi$.
\end{frame}

\section{Boolean abstraction}


\subsection{Definition}
\begin{frame}{A system with infinite state}

State = a single integer variable~$x$
\bigskip

Initial state~: $x = 0$

Transition: $x' = x+1$
\bigskip

Reachable states: $\NN$.
\bigskip

Prove that $x \geq 0$ is an invariant.
\bigskip

\stress{Cannot compute} reachable states by iterations: infinite state space!
\end{frame}


\begin{frame}{A finite state system}

State = a single integer variable~$x$
\bigskip

Initial state: $x = 0$

Transition: $x' = x+1 \land x < 10^{10}$
\bigskip

Reachable states: $0 \leq x \leq 10^{10}$
\bigskip

\stress{No hope} by explicit model-checking techniques (computing the $10^{10}$ reachable states).
\end{frame}

\begin{frame}{Abstraction}

Introduce 5 ``abstract states''
\begin{itemize}
\item $A$: $x < 0$
\item $B$: $x = 0$
\item $C$: $0 < x < 10^{10}$
\item $D$: $x = 10^{10}$
\item $E$: $x > 10^{10}$
\end{itemize}

Put an arrow between abstract states $P$ and $Q$ iff one can move
from $p \in P$ to $q \in Q$.
\bigskip

Example: can move from $A$ to $B$ because $\{ x = -1 \} \in A$, can move to $\{ x' = 0 \} \in B$.
\end{frame}

\begin{frame}{Resulting system}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
                    semithick]
%\tikzstyle{every state}=[fill=red,draw=none,text=white]

  \node[state] (A)              {$A$};
  \node[initial,state] (B) [below of=A] {$B$};
  \node[state]         (C) [right of=B] {$C$};
  \node[state]         (D) [right of=C] {$D$};
  \node[state]         (E) [right of=D] {$E$};
  \path (A) edge node {} (B)
        (B) edge node {} (C)
        (C) edge [loop above] node {} (C)
            edge node {} (D);
\end{tikzpicture}

\begin{itemize}
\item $A$: $x < 0$
\item $B$: $x = 0$
\item $C$: $0 < x < 10^{10}$
\item $D$: $x = 10^{10}$
\item $E$: $x > 10^{10}$
\end{itemize}

\stress{No concrete transition is forgotten} and thus $E$ is \stress{unreachable}.
\end{frame}

\begin{frame}{Other example}
Initial state: $x = 0$
Transition: $x' = x+2 \land x \neq 10^{10}$
\bigskip

Reachable states: $0 \leq x < 10^{10} \land x \bmod 2 = 0$.
\end{frame}

\begin{frame}{Abstract graph}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
                    semithick]
%\tikzstyle{every state}=[fill=red,draw=none,text=white]

  \node[state] (A)              {$A$};
  \node[initial, state] (B) [below of=A] {$B$};
  \node[state]         (C) [right of=B] {$C$};
  \node[state]         (D) [right of=C] {$D$};
  \node[state]         (E) [right of=D] {$E$};
  \path (A) edge node {} (B)
        (B) edge node {} (C)
        (C) edge [loop above] node {} (C)
            edge node {} (D)
            edge [bend left] node {} (E);
\end{tikzpicture}

\begin{itemize}
\item $A$: $x < 0$
\item $B$: $x = 0$
\item $C$: $0 < x < 10^{10}$
\item $D$: $x = 10^{10}$
\item $E$: $x > 10^{10}$
\end{itemize}

$C \rightarrow E$ since $(10^{10}-1) \rightarrow (10^{10}+1)$.
\end{frame}

% \begin{frame}[fragile]
% \frametitle{Other loop}

% \lstset{language=C++}
% \begin{lstlisting}
% bool b = false;
% int x = 0;
% while (x < 12) {
%   x = x+1;
%   b = x >= 10;
% }
% \end{lstlisting}

% We hope to prove $b = \true$ at the end. Invariant:

% $(\neg b \land 0 \leq x < 10) \lor (b \land 10 \leq x < 12)$.
% \end{frame}

\begin{frame}{Over-approximation}

More behaviors:
\begin{itemize}
\item $E$ is concretely reachable.
\item $E$ is abstractly reachable
\end{itemize}
\bigskip

The analysis fails to prove the true property ``$E$ unreachable''.

\stress{Incomplete} method.
\bigskip

Remark: works with a better abstraction ($x < 10^{10}-1$).
\end{frame}


\begin{frame}{Principles of predicate abstraction}

\begin{itemize}
\item A finite set of \stress{predicates} (e.g. arithmetic constraints).
\item Construct a \stress{finite} system of abstract transitions between abstract states.
\item Each abstract state labeled by predicates, e.g. ex. $x < 0$.
\item Put an abstract transition from $A$ to $B$ iff one can move from a state $a \in A$ to a state $b \in B$.
\item \stress{Correctness} if an abstract state is unreachable, then so are the corresponding concrete states
\end{itemize}
\end{frame}

\begin{frame}{How to construct the abstract system}
Abstract states $A: x < 0$ and $C : 0 < x < 10^{10}$, transition relation $x' = x+1 \land x < 10^{10}$, can we move from $A$ to $C$?
\medskip

Otherwise said: is there a solution to $x < 0 \land (x'= x+1 \land x < 10^{10}) \land x' > 0$?
\medskip

Use \stress{satisfiability modulo theory} (SMT-solving).
\end{frame}

\begin{frame}{Computing the graph}

\begin{itemize}
\item Abstract states are couples (program point, set of predicates)
\item Apply SMT-solving to insert or not insert arrows.
\item Check if \stress{bad states} are unreachable.
\item If they are, \stress{win!}
\end{itemize}
\bigskip

\dots and if they are reachable?
\begin{itemize}
\item Maybe the abstraction is badly chosen?
\item Maybe the property to prove (unreachability of bad states) is false?
\end{itemize}
\end{frame}

\subsection{Some more examples}
\begin{frame}[fragile]
\frametitle{Exemple}
\begin{lstlisting}[numbers=left]
x = 0;
while (x < 10) {
  x = x+1;
}
y = 0;
while (y < x) {
  y = y+1;
}
\end{lstlisting}

Try predicates $x < 0$, $x = 0$, $x > 0$, $x < 10$, $x = 10$, $x > 10$, $y < 0$, $y = 0$, $y > 0$, $y < x$, $y = x$, $y > x$.
\medskip

Note: 12 predicates, so in the worst case $2^{12} = 4096$ combinations, some of which impossible (cannot have both $x < 0$ and $x > 0$ at same time).
\end{frame}

\begin{frame}[fragile]
\frametitle{Abstract automaton}

\begin{minipage}{7cm}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.4cm,
                    semithick]

  \node[initial,state] (A)      {$L_1$};
  \node[state] (B) [right of=A] {$L_2$};
  \node[state] (B2)[right of=B] {$L_2'$};
  \node[state] (C) [below of=B2] {$L_5$};
  \node[state] (D) [left of=C] {$L_6$};
  \node[state] (D2) [left of=D] {$L_6'$};
  \node[state] (E) [left of=D2] {$L_9$};
  \path (A) edge node {} (B)
        (B) edge [loop above] node {} (B)
        (B) edge node {} (B2)
        (B2) edge node {} (C)
        (C) edge node {} (D)
        (D) edge [loop below] node {} (D)
        (D) edge node {} (D2)
        (D2) edge node {} (E);
\end{tikzpicture}
\end{minipage}
\begin{minipage}{4cm}
\begin{lstlisting}[numbers=left]
x = 0;
while (x<10)
  x = x+1;
}
y = 0;
while (y<x) {
  y = y+1;
}
\end{lstlisting}
\end{minipage}

$L_1$: line~1, $x=0$\\
$L_2$: line~2, $0 < x<10$\\
$L_2'$: line~2: $x=10$\\
$L_5$: line~5: $x=10$\\
$L_6$: line~6: $x=10 \land y<x$\\
$L_6'$: line~6: $x=10 \land y=x$\\
$L_9$: line~9: $x=10 \land y=x$
\end{frame}

\begin{frame}[fragile]
\frametitle{Attention}
\begin{lstlisting}[numbers=left]
x = 0;
while (x != 10) {
  x = x+2;
}
\end{lstlisting}
Syntactic choice of predicates ($x < 0$, $x = 0$, $x > 0$, $x < 10$, $x = 10$, $x > 10$).
\end{frame}

\begin{frame}{Some solution?}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.5cm,
                    semithick]
\node[initial,state] (A) {\begin{tabular}{c}L1\\x$=$0\end{tabular}};
\node[state] (B) [right of=A] {\begin{tabular}{c}L2\\x$=$0\end{tabular}};
\node[state] (B2) [right of=B] {\begin{tabular}{c}L2\\0$<$x$<$10\end{tabular}};
\node[state] (B3) [below of=B2] {\begin{tabular}{c}L2\\x$=$10\end{tabular}};
\node[state] (C) [left of=B3] {\begin{tabular}{c}L5\\x$=$10\end{tabular}};

 \path (A)  edge node {} (B)
       (B)  edge node {} (B2)
            edge [loop above] node {} (B)
       (B2) edge node {} (B3)
       (B3) edge node {} (C);
\end{tikzpicture}
\end{frame}

\begin{frame}{Why is this solution wrong?}

This solution is \stress{sound} since it collects all behaviors of the program.
\bigskip

But you realize this only because you already know (in your head)
the set of reachable states! (This is cheating.)

\bigskip

This solution is not \stress{inductive}: it is possible to move from a state
represented in the graph to one that isn't!
\end{frame}

\begin{frame}[fragile]
\frametitle{Attention}
\begin{lstlisting}[numbers=left]
x = 0;
while (x != 10) {
  x = x+2;
}
\end{lstlisting}

At line~2, abstraction says $0 < x < 10$, thus $x = 9$ for instance.
\bigskip

$x=9$ is inaccessible \emph{in the concrete systems}! You know it only because you computed the set of reachable states $\{0, 2, 4, 6, 8\}$.
\bigskip

Need a transition from $0 < x < 10$ ($x = 9$)
to a new state $x > 10$ ($x = 11$).
\end{frame}

\begin{frame}{Human intuition vs automated computation}

The human sees the simple program and computes the set of reachable states $\{0, 2, 4, 6, 8\}$ knowing $x$ should be even.
\medskip

Then projects onto predicates, and $x > 10$ unreachable.
\bigskip

Automated computation does not see that $x$ is even because it was not given the predicate $x \bmod 2 = 0$.
\end{frame}

\begin{frame}{Not convinced?}

Let $P$ be a program where Boolean $x$ is not mentioned. Consider:
$x := 0$;
$P$;
$x := 1$
\bigskip

Use predicates $x=0$ et $x=1$. Give a finite automaton for the behaviors of the program wrt~$x$\dots
\bigskip

Automaton with two states $x=0$, $x=1$. Simple, hey?
\end{frame}

\begin{frame}{A minimal automaton (not inductive)}

If \stress{$P$ terminates}:

\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.5cm,
                    semithick]
\node[initial,state] (A) {$x=0$};
\node[state] (B) [right of=A] {$x=1$};
\path (A)  edge [loop above] node {} (A);
\path (A)  edge node {} (B);
\end{tikzpicture}
\bigskip

If \stress{$P$ does not terminate}:

\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.5cm,
                    semithick]
\node[initial,state] (A) {$x=0$};
\path (A)  edge [loop above] node {} (A);
\end{tikzpicture}
\end{frame}

\subsection{Abstraction refinement}
\begin{frame}{Abstraction refinement}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
                    semithick]
%\tikzstyle{every state}=[fill=red,draw=none,text=white]

  \node[state] (A)              {$A$};
  \node[initial, state] (B) [below of=A] {$B$};
  \node[state]         (C) [right of=B] {$C$};
  \node[state]         (D) [right of=C] {$D$};
  \node[state]         (E) [right of=D] {$E$};
  \path (A) edge node {} (B)
        (B) edge node {} (C)
        (C) edge [loop above] node {} (C)
            edge node {} (D)
            edge [bend left] node {} (E);
\end{tikzpicture}

$x' = x+2 \land x \neq 10^{10}$
\bigskip

$E$ is reachable in the abstract and not in the concrete.

Would have been prevented using predicate $x < 10^{10}-1$. Can this be made automatic?
\bigskip

Yes: compute weakest precondition $wp(\neg E)$ for one step: $x \leq 10^{10} \land x+2 \leq 10^{10} \equiv x \leq 10^{10}-2$.

Add $x \leq 10^{10}-2$ as predicate and voilà.
\end{frame}

\begin{frame}{CEGAR}

Counterexample guided abstraction refinement
\bigskip

Generalize the idea «\,compute weakest precondition and add predicates\,».
\end{frame}

\begin{frame}{Some tools}

\begin{itemize}
\item Bounded model checking on C programs: CBMC
\item Predicate abstraction on C programs: Microsoft Device Driver Verifier [SLAM], BLAST
\item SMT-solvers: Yices (SRI), Z3 (Microsoft)
\end{itemize}
\end{frame}

\section{Intervals}

\begin{frame}{Inductive vs non-inductive invariants}
\begin{center}
\includegraphics[height=5cm]{unstable}
\end{center}

\textcolor{red}{Reachable states}\\
\textcolor{blue}{Least invariant as product of intervals} \onslide<2->{not inductive}\\
\textcolor{green}{Least invariant as convex polyhedron} \onslide<3->{inductive}
\end{frame}

\begin{frame}[fragile]
\frametitle{Best invariant in domain not computable}

\begin{lstlisting}
P();
x=0;
\end{lstlisting}

Best invariant at end of program, as interval?
\bigskip
\pause

$[0,0]$ iff \lstinline|P()| terminates

$\emptyset$ iff \lstinline|P()| does not terminate
\bigskip

Entails solving the halting problem.
\end{frame}

\begin{frame}[fragile]
\frametitle{Recall the idea}

Try to compute an interval for each variable at each program point using \stress{interval arithmetic}~:

\begin{lstlisting}
assume(x >= 0 && x<= 1);
assume(y >= 2 && y= 3);
assume(z >= 3 && z= 4);
t = (x+y) * z;
\end{lstlisting}

Interval for~$z$? \pause \stress{$[6,16]$}
\end{frame}

\begin{frame}{Why is this interesting?}

Let $t(0..10)$ an array.

Program writes to $t(i)$.
\bigskip

We must know whether $0 \leq i \leq 10$, thus know an
\stress{interval} over~$i$.
\end{frame}

\begin{frame}[fragile]
\frametitle{Again\dots}

\begin{lstlisting}
assume(x >= 0 && x <= 1);
y = x;
z = x-y;
\end{lstlisting}

\begin{itemize}
\item The human (intelligent) sees $z = 0$ thus interval $[0,0]$, taking into account $y=x$.
\item Interval arithmetic does not see $z = 0$ because it does not take $y=x$ into account.
\end{itemize}
\end{frame}

\begin{frame}{How to track relations}

Using \stress{relational domains}.
\bigskip

E.g.: keep
\begin{itemize}
\item for each variable an interval
\item for each pair of variables $(x,y)$ an information $x -y \leq C$.
\item (One obtains $x=y$ by $x-y \leq 0$ and $y-x \leq 0$.)
\end{itemize}
\bigskip

How to \stress{compute} on that?
\end{frame}

\begin{frame}{Bounds on differences}

\begin{center}
\includegraphics{dbm1}
\end{center}
\end{frame}

\begin{frame}{Practical example}

Suppose $x - y \leq 4$, computation is $z = x+3$, then we know $z  -y \leq 7$.
\bigskip

Suppose $x - z \leq 20$, that $x - y \leq 4$ and that $y - z \leq 6$, then we know $x -z \leq 10$.
\bigskip

We know how to \stress{compute} on these relations (transitive closure / shortest path).

On our example, obtain $z = 0$.
\end{frame}

\begin{frame}{Why this is useful}

Let $t(0..\stress{n})$ an array in the program.

The program writes $t(i)$.
\bigskip

Need to know whether $0 \leq i \leq n$, otherwise said find bounds on
$i$ and on $n-i$\dots
\end{frame}


\begin{frame}{Can we do better?}

How about tracking relations such as $2x+3y \leq 6$?
\bigskip

At a given program point, a set of \stress{linear inequalities}.
\bigskip

In other words, a \stress{convex polyhedron}.
\end{frame}

\begin{frame}{Example of polyhedron}
\begin{center}
\includegraphics[height=7cm]{polyedre01}
\end{center}
\end{frame}

\begin{frame}{Caveat}

(In general) The more precise we are, the higher the costs.

For each line of code:
\begin{itemize}
\item Intervals: algorithms $O(n)$, $n$ number of variables.
\item Differences $x-y \leq C$~: algorithms $O(n^3)$
\item Octagons $\pm x \pm y \leq C$ (Min\'e)~: algorithms $O(n^3)$
\item Polyhedra (Cousot / Halbwachs): algorithms often $O(2^n)$.
\end{itemize}
\bigskip

On short examples with few variables, ok\dots But in general?
\end{frame}

\begin{frame}{Even linear may not be fast enough}

Fly-by-wire control code from Airbus:

\begin{itemize}
\item Main control loop
\item Number of tests linear in length $n$ of code
\item Number of variables linear in length $n$ of code (global state)
\item Complexity of naive convex hull on products of intervals linear in number of variables
\end{itemize}
\pause

\finger Cost per iteration in $n^2$
\end{frame}

\begin{frame}[fragile]
\frametitle{Absolute value}

\begin{lstlisting}
y = abs(x);  /* valeur absolue */
if (y >= 1) {
  assert(x != 0);
}
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Interval expansion}

Intervals:

\begin{lstlisting}
/* -1000 <= x <= 2000 */
if (x < 0) y = -x; /* 0 <= y <= 1000 */
else y = x; /* 0 <= y <= 2000 */

if (y >= 1) { /* 1 <= y <= 2000 */
  assert(x != 0); /* -1000 <= x <= 2000 !!! */
}
\end{lstlisting}
\end{frame}

\begin{frame}{Polyhedra}

Branch $x \geq 0$

\begin{center}
\includegraphics[height=6cm]{abs_polyedre1}
\end{center}
\end{frame}

\begin{frame}{Other branch}

Branch $x < 0$

\begin{center}
\includegraphics[height=6cm]{abs_polyedre2}
\end{center}
\end{frame}


\begin{frame}{After first test}


$y=|x|$ = union of the two red lines. Not a convex.

Convex hull = pink polyhedron

\begin{center}
\includegraphics[height=5cm]{abs_polyedre_lub}
\end{center}
\end{frame}

\begin{frame}{At second test}

Note: includes $(x,y) = (0, 1)$.

\begin{center}
\includegraphics[height=6cm]{abs_polyedre_final}
\end{center}
\end{frame}

\begin{frame}{Disjunction}

Possible if we do a union of two polyhedra:
\begin{itemize}
\item $x \geq 0 \land y = x$
\item $x < 0 \land y = -x$
\end{itemize}
\bigskip

But with $n$ tests?
\end{frame}

\begin{frame}[fragile]
\frametitle{Two tests}
\begin{lstlisting}
if (x >= 0) y=x; else y= -x;
if (y >= 1) z=y+1; else z=y;
\end{lstlisting}

4 polyhedra = costly computations
\begin{center}
\includegraphics[height=4cm]{disjonctive2tests}
\end{center}
\end{frame}

\begin{frame}{Two tests, convex hull}

More imprecise:
\begin{center}
\includegraphics[height=6cm]{disjonctive2tests_cvx}
\end{center}
\end{frame}

\begin{frame}{Sources of imprecision}
\begin{itemize}
\item Need to distinguish \stress{each path} and compute one polyhedron for each.
\item But $2^n$ paths.
\item \stress{Too costly} if done naively.
\item In current tools, not implemented.
\item \finger explains some imprecisions.
\end{itemize}
\end{frame}

\begin{frame}{Current research}

In the last few years articles propose methods distinguishing paths.
\bigskip

Use of SMT-solving techniques to cut the exponential cost:

\medskip

Only look at ``useful'' paths.
\end{frame}

\section{Extrapolation}

\begin{frame}[fragile]
\frametitle{Loops?}

Push intervals / polyhedra forward\dots

\begin{lstlisting}
int x=0;
while (x<1000) {
  x=x+1;
}
\end{lstlisting}

Loop iterations $[0,0]$, $[0,1]$, $[0,2]$, $[0,3]$,\dots
\medskip

How? $\phi(X) = \textrm{état initial} \sqcup \post(X)$, thus
$\phi([a,b]) = \{ 0 \} \sqcup [a+1,\min(b,999)+1]$

\bigskip

\stress{When do we stop?} Wait 1000 iterations? No.
\end{frame}

\begin{frame}[fragile]
\frametitle{One solution\dots}

\stress{Extrapolation!}
\bigskip

$[0,0]$, $[0,1]$, $[0,2]$, $[0,3]$ $\rightarrow$ $[0,+\infty)$
\bigskip

Push interval:
\begin{lstlisting}
int x=0; /* [0, 0] */
while /* [0, +infty) (x<1000) {
  /* [0, 999] */
  x=x+1;
  /* [1, 1000] */
}
\end{lstlisting}

Yes! $[0,\infty[$ is stable!
\end{frame}

\begin{frame}[fragile]
\frametitle{Mediocre results}

Expected: \stress{$[0,999]$}.

Obtained \stress{$[0,+\infty)$}.
\bigskip
\pause

Run one more iteration of the loop:
\begin{lstlisting}
[0, +infty) (x<1000)
  /* [0, 999] */
  x=x+1;
  /* [1, 1000] */
\end{lstlisting}

Obtain $\{ 0 \} \sqcup [1, 1000] = [0,1000]$.
\end{frame}

\begin{frame}[fragile]
\frametitle{Narrowing}

\begin{lstlisting}
int x=0; /* [0, 0] */
while /* [0,1000] (x<1000) {
  /* [0, 999] */
  x=x+1;
  /* [1, 1000] */
}
\end{lstlisting}

Yes! $[0,1000]$ is an inductive invariant!
\end{frame}

\begin{frame}{Stabilization}

Look for a set (polyhedron, intervals)
\begin{itemize}
\item Containing initial values for the loop.
\item \stress{Inductive}: if valid at one iteration, valid at the next.
\end{itemize}
\bigskip

Look for $X$ such that
$\phi(X) \subseteq X$ with $\phi(X) = \textrm{états initiaux} \cup
\post(X)$

$\post(X)$ = states reachable from $X$ in one loop iteration
\medskip

\stress{Any} inductive invariant. (Not necessarily the least one.)
\end{frame}

\begin{frame}{Computing the inductive invariant}

We don't know how to compute $\post(P)$ with $P$ interval / polyhedron
in general.

(The loop body may be complex, with tests\dots)
\medskip

Replace computation by simpler over-approximation
$\post(X) \subseteq \abstr{\post}(X)$.
\medskip

Cannot do $\cup$ over polyhedra, do $\sqcup$ (convex hull)

Thus computation:
$\abstr{\phi}(X) = \text{initial states} \sqcup \abstr{\post}(X)$

Instead of
$\phi(X) \subseteq X$ with $\phi(X) = \textrm{initial states} \cup \post(X)$
\end{frame}

\begin{frame}{All the time, over-approximation}

$\phi(X) \subseteq \abstr{\phi}(X)$ so
$\lfp \phi \subseteq \lfp \abstr{\phi}$

(work out the math, using $\lfp \psi = \inf \{ X \mid \psi(X) \subseteq X \}$)
\bigskip

In the end, \stress{over-approximation} of the least fixed point of~$\phi$.
\end{frame}

\begin{frame}{Graphical vision}

Dark blue = concrete reachable states after $\leq 1$ loop iteration

Light blue =  concrete reachable states after $\leq 2$ loop iterations

Dark red = over-approximated states after $\leq 1$ loop iteration

Light red =  over-approximated states after $\leq 2$ loop iterations

\begin{center}
\includegraphics[height=5cm]{widening_polyhedra_concrete}
\end{center}
\end{frame}

\begin{frame}{Extrapolation}

\begin{center}
\includegraphics[height=6cm]{widening_polyhedra}
\end{center}
\end{frame}

\begin{frame}{Where to extrapolate?}

Extrapolation needed for \stress{termination}: avoid iterating infinitely on
cycles in control flow graph.
\bigskip

Need to extrapolate only at a \stress{limited set of points} that break all cycles.

\bigskip

Choice of minimal set NP-complete.

Minimal does not necessarily mean better precision.

\smallskip

Simple method: depth-first search for cycles.
\end{frame}

\begin{frame}{Depth-first search}

\begin{minipage}{3cm}
\begin{tikzpicture}[node distance=2cm]
\node [block] (init) { init };
\node [block, below of=init] (loop1) {loop1} ;
\node [block, below of=loop1] (loop2) {loop2} ;

\path [edge] (init) edge (loop1);
\path [edge] (loop1) edge (loop2);
\path [edge, bend right=40] (loop2) edge (loop1);
\path [edge, bend left=40] (loop2) edge (init);
\end{tikzpicture}
\end{minipage}\hfill
$\longrightarrow$\hfill
\begin{minipage}{7cm}
Depth-first search:\\
init $\rightarrow$ loop1 $\rightarrow$ loop2  $\rightarrow$ init\\
backtrack to loop2, then loop2  $\rightarrow$ loop1
\medskip

Mark init, loop1 as widening nodes

\medskip
\begin{tikzpicture}[node distance=2cm]
\node [loopblock] (init) { init };
\node [loopblock, below of=init] (loop1) {loop1} ;
\node [block, below of=loop1] (loop2) {loop2} ;

\path [edge] (init) edge (loop1);
\path [edge] (loop1) edge (loop2);
\path [edge, bend right=40] (loop2) edge (loop1);
\path [edge, bend left=40] (loop2) edge (init);
\end{tikzpicture}
\end{minipage}
\end{frame}

\begin{frame}{Minimal set}

\begin{minipage}{3cm}
\begin{tikzpicture}[node distance=2cm]
\node [block] (init) { init };
\node [block, below of=init] (loop1) {loop1} ;
\node [block, below of=loop1] (loop2) {loop2} ;

\path [edge] (init) edge (loop1);
\path [edge] (loop1) edge (loop2);
\path [edge, bend right=40] (loop2) edge (loop1);
\path [edge, bend left=40] (loop2) edge (init);
\end{tikzpicture}
\end{minipage}\hfill
$\longrightarrow$\hfill
\begin{minipage}{7cm}
\begin{tikzpicture}[node distance=2cm]
\node [block] (init) { init };
\node [loopblock, below of=init] (loop1) {loop1} ;
\node [block, below of=loop1] (loop2) {loop2} ;

\path [edge] (init) edge (loop1);
\path [edge] (loop1) edge (loop2);
\path [edge, bend right=40] (loop2) edge (loop1);
\path [edge, bend left=40] (loop2) edge (init);
\end{tikzpicture}
\end{minipage}
\end{frame}

\begin{frame}[fragile]
\frametitle{A bad invariant}

\begin{lstlisting}
i = 0;
while (true) {
  if (random()) {
    i = i+1;
    if (i >= 100) i = 0;
  }
}
\end{lstlisting}

Analysis using widening will yield
\pause

$[0,0]$, $[0,1]$, $[0,2]$, \dots, $[0,+\infty)$
\pause

Narrowing yields
\pause

$[0,+\infty)$
\end{frame}

\begin{frame}[fragile]
\frametitle{A bigger precondition}

\begin{lstlisting}
i = [0, 99];
while (true) {
  if (random()) {
    i = i+1;
    if (i >= 100) i = 0;
  }
}
\end{lstlisting}

Analysis using widening will yield
\pause

$[0,99]$, fixpoint reached
\bigskip

Note: with \stress{larger precondition}, smaller inferred invariant.

Analysis with widening is \stress{non monotonic}.
\end{frame}

\begin{frame}[fragile]
\frametitle{Workaround: widening with thresholds}

Syntactic detection of comparisons

\begin{lstlisting}
i = 0;
while (true) {
  if (random()) {
    i = i+1;
    if (i >= 100) i = 0;
  }
}
\end{lstlisting}

Detect \stress{\lstinline|i >= 100|}, so 99 ``magic value''.

Widening: $[0,0]$, $[0,1]$, \dots, $[0,99]$

\bigskip

Applicable to intervals, octagons, polyhedra.
\end{frame}

\begin{frame}{Consequences}

\begin{itemize}
\item Over-approximate during computations (even without loops).
\item Over-approximation during widening.
\item Thus obtain \stress{super-}set of reachable states.
\item This super-set is an \stress{inductive invariant} (cannot exit from it).
\end{itemize}
\end{frame}

\begin{frame}{Practical consequences}

\begin{itemize}
\item Cannot prove that a problem truly happens.

Example: interval $i \in [0,20]$ for access $t(0..10)$, is the interval exact?

\item Yet sure that all potential problems are detected (over-approximation of problems).

\item Let $B$ be the set of bad states. $\abstr{X} \cap B \neq \emptyset$: \textcolor{orange}{``ORANGE''}

\item If $\abstr{X} \subseteq B$, \textcolor{red}{``RED''}.

\item What do orange vs red mean?
\end{itemize}
\end{frame}

\section{Backward / forward}

\begin{frame}[fragile]
\frametitle{Simple ``avoid zero'' example}
\begin{minipage}{6cm}
\begin{lstlisting}[numbers=right]
if (x >= 0) {
  y = x;
} else {
  y = -x;
}
if (y >= 1) {
  assert(x != 0);
}
\end{lstlisting}

Forward analysis with polyhedra:\\
$P_2 = \{ x \geq 0 \land y = x \}$\\
$P_4 = \{ x < 0 \land y = x \}$\\
$P_5 = P_2 \sqcup P_4 = \{ y \geq x \land y \geq -x \}$\\
$P_6 = P_5 \cap \{ y \geq 1 \}$
\end{minipage}\hfill%
\begin{tabular}{c}
\includegraphics[width=2.5cm]{abs_polyedre1} \\
\includegraphics[width=2.5cm]{abs_polyedre2}\\
\includegraphics[width=2.5cm]{abs_polyedre_lub}\\
\includegraphics[width=2.5cm]{abs_polyedre_final}\\
\end{tabular}
\end{frame}

\begin{frame}{Backward analysis}
Move backward from $x = 0$ ``bad state'', intersect each time with analysis result from forward.

\begin{center}
\begin{tabular}{cc}
\includegraphics[width=4.5cm]{abs_polyedre_final_x0}&
\includegraphics[width=4.5cm]{abs_polyedre_lub_x0}\\
\includegraphics[width=4.5cm]{abs_polyedre1_x0}&
\includegraphics[width=4.5cm]{abs_polyedre2_x0}\\
\end{tabular}
\end{center}
\end{frame}

\begin{frame}{Idea}

Reachable = reachable from start\\
Co-reachable = co-reachable from a certain error condition
\medskip

Forward: compute superset of \stress{reachable} states

Forward then backward: compute superset of \stress{reachable} $\cap$ \stress{co-reachable}
\bigskip

and then

\smallskip

Forward then backward then forward
etc.

Downwards iterations (every time, intersect with preceding).
\end{frame}

\begin{frame}[fragile]
\frametitle{Backward analysis over intervals}

\begin{lstlisting}
z = x-y;
\end{lstlisting}

If you know $z \in [0,3]$ at the end, what do you get over $x$ and $y$?
\pause

Nothing.
\end{frame}

\begin{frame}[fragile]
\frametitle{Forward-backward analysis over intervals}

\begin{lstlisting}
z = x-y;
\end{lstlisting}

If you know $z \in [0,3]$ at the end, and $x \in [0,2]$, what do you get over $y$?
\pause

$y = x-z$ thus $y \in [-3,2]$
\end{frame}

\begin{frame}{Forward / backward}

Backward analysis alone: hardly usable on intervals, better for relational domains

Much better if preceded by forward analysis
\bigskip

Forward analysis first: don't worry about states obviously unreachable

Backward analysis first:  don't worry about states obviously not co-reachable
\bigskip

In general, forward then backward.
\end{frame}

\section{Direct computations of invariants}

\begin{frame}[fragile]
\frametitle{A simple loop}

\begin{lstlisting}
i = 0;
while (i < 10000) {
   i = i+1;
}
\end{lstlisting}

Look for $u$ such that $i \leq u$ inductive in the loop.

$u \geq 0$ (initial state)

$u \geq \min(u, 9999)+1$ (guard $i < 10000$ and assignment $i := i+1$)
\bigskip

Look for least solution. But then
$u = \max(0, \min(u, 9999)+1)$.
\end{frame}


\begin{frame}[fragile]
\frametitle{An exponential loop}

\begin{lstlisting}
i = 1;
while (i < 10000) {
   i = i*2;
}
\end{lstlisting}

Look for $u$ such that $i \leq u$ inductive in the loop.

$u \geq 1$ (initial state)

$u \geq 2\min(u, 9999)$ (guard $i < 10000$ and assignment $i := 2i$)
\bigskip

Look for least solution. But then
$u = \max(1, 2\min(u, 9999))$.
\end{frame}

\begin{frame}{Min-max system}

Invariants of the form $x \in [-L_x,U_x]$ for variable $x$.
\bigskip

Least solution of system of equations with lhs the $L_x, U_x$, with rhs
\begin{enumerate}
\item Monotone linear combinations (+ constants) of the $L_y,U_y$
\item min (from guards)
\item max (from merge points in control flow graph)
\end{enumerate}

e.g. $u = \max(0, \min(u, 9999)+1)$

e.g. $u = \max(1, 2\min(u, 9999))$
\end{frame}

\begin{frame}{Solving}

Let $L_x, U_x, L_y, U_y, \dots$ be a solution of the equalities.
\smallskip

Then for any subexpression $\min(a, b)$, $\min(a, b)_{| L_x, U_x, L_y, U_y, \dots}$ is either $a_{| L_x, U_x, L_y, U_y, \dots}$ or $b_{| L_x, U_x, L_y, U_y, \dots}$.
\bigskip

Case-splitting: if $n$ min operators, $2^n$ cases. Each case yields a
system with rhs
\begin{enumerate}
\item Monotone linear combinations (+ constants) of the $L_y,U_y$
\item max (from merge points in control flow graph)
\end{enumerate}
\end{frame}

\begin{frame}{Solving a max-system}
Everything monotone, move max to the outside. E.g.

$\max(2U_x+1,U_y)+\max(U_x+3,U_y+1) = \max(3U_x+4,2U_x+U_y+2,U_y+U_x+3,2U_y+1)$.

\bigskip

Then solve for least solution of system of equations like $U_x = \max(3U_x+4,2U_x+U_y+2,U_y+U_x+3,2U_y+1)$.

\bigskip

Same as least solution of equations like $U_x \geq  \max(3U_x+4,2U_x+U_y+2,U_y+U_x+3,2U_y+1)$.

Equivalent to
$U_x \geq 3U_x+4 \land U_x \geq 2U_x+U_y+2 \geq U_y+U_x+3 \geq 2U_y+1$
\end{frame}

\begin{frame}{Least solution of system of inequalities}
\begin{equation*}\left\{
\begin{array}{l}
U_x \geq \dots\\
U_x \geq \dots\\
L_x \geq \dots\\
U_y \geq \dots\\
L_y \geq \dots
\end{array}
\right.
\end{equation*}

Least solution for $(U_x,L_x,U_y,L_y,\dots) \leq (U'_x,L'_x,U'_y,L'_y,\dots)$
variable-wise same as least solution for
$U_x + L_x + U_y + L_y$.
\bigskip

\stress{Linear programming} (+ trick for $+\infty$)
\end{frame}

\begin{frame}{Executive summary}

\begin{itemize}
\item For interval constraints
\item or more generally $AX \leq B$, $A$ fixed, defined by~$B$
\item with linear guards and assignments
\item can compute least inductive invariant of the selected form
\item using an exponential number of linear programming calls
\end{itemize}
\end{frame}

\begin{frame}{Example~1}
$u = \max(0, \min(u, 9999)+1)$
\bigskip

First choose: $\min(u, 9999) = u$.

Equation becomes: $u = \max(0, u+1)$.

Thus $u \geq 0$, $u \geq u+1$.

Only solution: $u = +\infty$.
\bigskip

Then choose: $\min(u, 9999) = 9999$.

Equation becomes: $u = 10000$.
\bigskip

Least solution is $u = 10000$.
\end{frame}

\begin{frame}{Example~2}
e.g. $u = \max(1, 2\min(u, 9999))$
\bigskip

First choose: $\min(u, 9999) = u$.

Equation becomes: $u = \max(1, 2u)$.

Thus $u \geq 1$, $u \geq 2u$.

Only solution $u = +\infty$.
\bigskip

Then choose: $\min(u, 9999) = 9999$.

Equation becomes: $u = \max(1, 2\times9999)$.

Only solution: $u = 19998$.
\end{frame}

\begin{frame}{Remarks on example~2}

Seems like least interval invariant would be $u \leq 16384$ (first power of two above $10000$).

But this invariant is \stress{not inductive}: take $i = 9999 \leq 16384$, then $2i = 19998 > 16384$.
\bigskip

Need something like $\exists k\geq 0~ i = 2^k$
\end{frame}

\begin{frame}{Max-policy iteration}
(\'Eric Goubault's group)
\bigskip

In practice: don't enumerate all $2^n$ max combinations.

Choose one. Solve problem. See if some of the ``max'' selects wrong argument.
If they do select new ``max'' argument.
\bigskip

Process terminates on a fixpoint of the original equations.

Not necessarily the least one.
\end{frame}

\section{Things not covered}

\begin{frame}{Outside numerical values}

Data structures:
\begin{itemize}
\item predicate abstraction
\item finite automata\dots
\end{itemize}
\bigskip

Termination analysis
\bigskip

Timing (WCET): models for cache and pipeline
\end{frame}

\begin{frame}{Recent techniques}
\begin{itemize}
\item Path-focused analysis
\item Synthesis of transfer function from specification
\item Reductions to mathematical programming
\end{itemize}
\end{frame}

\section{Executive summary}
\begin{frame}{Outside of numerics}

Pointers, arrays, memory threads\dots

\bigskip

E.g. representing tree / graphs using automata

Widening = limitation in the number of states when computing bisimulation
(Myhill-Nerode minimization of DFA)
\end{frame}

\begin{frame}{Important points}
\begin{itemize}
\item The computer is stupid, it does not ``see'' why a program works.
\item Normal, everything important is \stress{undecidable algorithmically} (or of \stress{high complexity}).
\item Look for inductive invariants that can be \stress{proved automatically} (e.g. by propagation of intervals or polyhedra).
\item They over-approximate the reachable states, thus the safety violations.
\end{itemize}
\end{frame}

\begin{frame}{Success stories}


\begin{itemize}
\item \stress{Microsoft SLAM} / Device driver verifier --- predicate abstraction, checks the respect of Windows API in device drivers

\item \stress{PolySpace Verifier}
\item \stress{Astr\'ee}, with specific control numerical relations --- A340, A380 (Airbus), ATV (EADS Astrium / ESA), etc.
\item \stress{Absint}, worst case execution time (WCET) with cache and pipelines
\end{itemize}
\end{frame}

\end{document}