\documentclass{beamer}
%\documentclass[handout]{beamer}

\usepackage{beamerjcf}
\usepackage{tikz}

\definecolor{kwblue}{rgb}{0.67,0.12,0.92}

\newcommand{\DEMO}{\begin{center}\emph{DEMO}\end{center}}
\newcommand{\kw}[1]{{\color{blue}#1}}
\newcommand{\minelt}[1]{\ensuremath{\mathit{min\_elt}(#1)}}
\newcommand{\cit}[1]{{\color{darkgreen}[#1]}}

\newcommand{\Caduceus}{\textsc{Caduceus}}
\newcommand{\Krakatoa}{\textsc{Krakatoa}}
\newcommand{\Why}{\textsc{Why}}
\newcommand{\Jessie}{\textsc{Jessie}}
\newcommand{\Java}{\textsc{Java}}
\newcommand{\JavaCard}{\textsc{Java Card}}
\newcommand{\C}{\textsc{C}}

\begin{document}

\title[SMT Solvers and the Why platform]{Using SMT Solvers  \\ 
for Deductive Verification of C and Java Programs}
\author[Jean-Christophe Filli\^atre]{Jean-Christophe Filli\^atre}
\institute{CNRS \\ Orsay, France}
\date{SMT, July 7, 2008}

\begin{frame}
  \titlepage
  \pgfimage[height=8mm]{cnrs-logo}\hfill
  \pgfimage[height=6mm]{inriafuturslogoshort}\hfill
  \pgfimage[height=10mm]{lrilogo}\hfill
  \pgfimage[height=8mm]{upsudlogo}
\end{frame}

\begin{frame}
  \frametitle{The ProVal Project --- \url{http://proval.lri.fr/}}

  \begin{itemize}
  \item foundations of \emph{ProVal}: the Coq project
    \begin{itemize}
    \item type theory: type $\simeq$ logic specification
  \item Curry-Howard isomorphism: proof $\simeq$ program
  \item \emph{functional} programs only
  \end{itemize}

  \Item goals of \emph{ProVal}: 
    \begin{itemize}
    \item to deal with \emph{imperative programs} (C, Java)
    \item to apply our methods to \emph{industrial cases}
    \end{itemize}
  \end{itemize}

\end{frame}

\begin{frame}
    \frametitle{Brief History}

  \begin{itemize}
  \item 1999: a first approach for programs with side effects in Coq

  \item 2000-2003: EU project Verificard (verification of Java Card
    applets with industrial partners GemPlus, Schlumberger)

  \item 2001-: stand-alone \Why{} tool, to use both automatic and
    interactive provers 

  \item 2003-: \Krakatoa{} tool for \Java\ programs

  \item 2004-: \Caduceus{} tool for C programs

  \item 2007: The \Why{} platform
  \end{itemize}

\end{frame}


\begin{frame}\frametitle{Outline}
  \begin{enumerate}
  \item overview of the Why platform
  \Item SMT solvers and program verification
    \begin{itemize}
    \item theories of interest for program verification
    \end{itemize}
  \Item SMT-lib and SMT-comp
  \end{enumerate}
\end{frame}

%%%% 1 overview of the Why platform %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}\frametitle{Overview of the Why Platform}

  \begin{itemize}
  \item 
    general \emph{goal}: prove behavioral properties of \emph{pointer
      programs}

\bigskip
  \item 
    pointer program = program manipulating data structures with
    \emph{in-place mutable fields}

\bigskip
  \item we currently focus on \emph{C} and \emph{Java} programs
  \end{itemize}
\end{frame}

\begin{frame}\frametitle{What Kind of Properties}
  two kinds

  \begin{itemize}
  \item \emph{safety}, that is
    \begin{itemize}
    \item no null pointer dereference
    \item no array access out of bounds (no buffer overflow)
    \item no division by zero
    \item no arithmetic overflow
    \item termination
    \end{itemize}
  \Item \emph{behavioral correctness}
    \begin{itemize}
    \item the program does what it is expected to do
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}\frametitle{Principles}
  \begin{itemize}

  \item 
    specification as \emph{annotations} at the source code level
    \begin{itemize}
    \item Java: an extension of JML (Java Modeling Language) 
    \item C: our own language (mostly JML-inspired) 
    \end{itemize}

    \bigskip
  \item 
    generation of \emph{verification conditions} (VCs)

    \begin{itemize}
    \item 
      using Hoare logic / weakest preconditions
      
    \item 
      similar approaches: static ESC/Java, SPEC\#, B method, etc.
    \end{itemize}

  \bigskip
  \item \emph{multi-prover} approach
    \begin{itemize}
    \item off-the-shelf provers, as many as possible
    \item automatic provers (Alt-Ergo, Simplify, Yices, Z3, CVC3, etc.)
    \item proof assistants (Coq, PVS, Isabelle/HOL, etc.)
    \end{itemize}

  \end{itemize}
\end{frame}

% binary search

\begin{frame}\frametitle{A Toy Example: Binary Search}

  \emph{binary search}: search a sorted array of integers for a given value

  \bigskip
  famous example; see J. Bentley's \textit{Programming Pearls} \par
  most programmers are wrong on their first attempt to write binary search
\end{frame}

\begin{frame}\frametitle{Binary Search (C code)}
\begin{c}
int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1;
  while (l <= u ) {
    int m = (l + u) / 2;
    if (t[m] < v)
      l = m + 1;
    else if (t[m] > v)
      u = m - 1;
    else 
      return m;
  }
  return -1;
}
\end{c}
\end{frame}

\begin{frame}\frametitle{Binary Search: Safety}

\begin{itemize}
\item no division by zero
\item no array access out of bounds
\item termination
\end{itemize}

\bigskip

\begin{c}
/*@ requires n >= 0 && \valid_range(t,0,n-1) */
int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1;
  /*@ invariant 0 <= l && u <= n-1 
    @ variant   u-l
    @*/
  while (l <= u ) {
    ...
}
\end{c}
\DEMO
\end{frame}

\begin{frame}\frametitle{Binary Search: Behavioral Specification}
\begin{c}
/*@ requires 
  @   n >= 0 && \valid_range(t,0,n-1) &&
  @   \forall int k1, int k2; 
  @     0 <= k1 <= k2 <= n-1 => t[k1] <= t[k2]
  @ ensures
  @   (\result >= 0 && t[\result] == v) ||
  @   (\result == -1 && 
  @      \forall int k; 0 <= k < n => t[k] != v)
  @*/
int binary_search(int* t, int n, int v) {
  ...
}
\end{c}
\end{frame}

\begin{frame}\frametitle{Binary Search: Behavioral Specification (cont'd)}

requires a stronger invariant

\begin{c}
int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1;
  /*@ invariant 
    @   0 <= l && u <= n-1 && 
    @   \forall int k; 
    @      0 <= k < n => t[k] == v => l <= k <= u
    @ variant u-l 
    @*/
  while (l <= u ) {
    ...
  }
}
\end{c}
\DEMO
\end{frame}

\begin{frame}\frametitle{Binary Search: Arithmetic Overflows}

finally, let's prove that there is no arithmetic overflow...
\pause \emph{there is one!}

\bigskip

in statement
\begin{c}
  int m = (l + u) / 2;
\end{c}
a possible overflow is signaled; a possible fix is
\begin{c}
  int m = l + (u - l) / 2;
\end{c}

\bigskip

see 
    \begin{itemize}
    \item Google: ``Read All About It: Nearly All Binary Searches and
      Mergesorts are Broken''
    \item ``Types, Bytes, and Separation Logic'' POPL'07
    \end{itemize}

\end{frame}

\begin{frame}
  \frametitle{Verification Technique}

  we use a standard technology (component-as-array memory model,
  weakest preconditions, etc.) 

  \bigskip
  two specific issues:
  \begin{itemize}
  \item how to share the effort which is common to C and Java

  \item how to use many different theorem provers
  \end{itemize}

  \bigskip
  our solution: the use of an intermediate language, \emph{Why}, which is
  \begin{itemize}
  \item a VC generator
  \item a common front-end to various provers
  \end{itemize}
\end{frame}

\begin{frame}\frametitle{Platform Overview}
  \includegraphics[width=\textwidth]{./platform.pdf}
\end{frame}

\begin{frame}\frametitle{Why: a Verification Condition Generator}
  \emph{Why} is a \emph{verification condition generator} for a
  language with
  \begin{itemize}
  \item variables containing pure values, 
    no alias (\url{~} Hoare-logic language)
  \item usual control structures (loops, tests, etc.)
  \item exceptions
  \item (possibly recursive) functions
  \item polymorphic first-order logic with equality and arithmetic 
  \end{itemize}
  Why is similar to Boogie (SPEC\#{} project)

  \bigskip\bigskip
  Why is also responsible for \emph{translating} verification conditions to
  the \emph{native logics} of all provers
\end{frame}

\begin{frame}\frametitle{Generating the Verification Conditions}
  \begin{center}
  \includegraphics[width=0.9\textwidth]{./cad_why.pdf}
  \end{center}
\end{frame}

% why = aussi notre langage commun pour parler aux prouveurs

%%% 2 SMT solvers and program verification

\begin{frame}
  \begin{center}
    \hrulefill\\
    \Large\emph{SMT Solvers and Program Verification}
  \end{center}
\end{frame}

\begin{frame}\frametitle{Disclaimer}
  don't be mistaken by the remaining of this talk; \par

  \bigskip
  I do think that
  \begin{itemize}
  \item SMT solvers are great tools!
  \item SMT-lib is definitely a good idea
  \item SMT-comp helps improving the quality of SMT solvers
  \end{itemize}
\end{frame}

% 2a which theories for program verification

\begin{frame}\frametitle{Which Logics for Program Verification}
  SMT solvers provide
  \begin{itemize}
  \item \emph{first-order logic with equality}
    \begin{itemize}
    \item memory models, user axiomatic models, etc.
    \end{itemize}
  \item \emph{integer/rational/real linear arithmetic}
    \begin{itemize}
    \item integer arithmetic: array indices, pointer arithmetic, etc.
    \end{itemize}

  \Item \emph{applicative arrays}
  \begin{itemize}
  \item axiomatic approach is equally efficient
  \item extensionality is not needed in practice
  \end{itemize}

  \Item \emph{fixed-size bit vectors}
  \begin{itemize}
  \item a too restrictive interface
  \end{itemize}
  \item \emph{tuples}, \emph{records}, \emph{inductive data types}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Which Logics for Program Verification}

  relevant theories for program verification can be different
  \begin{itemize}
  \item \emph{non-linear arithmetic}
  \item \emph{finite sets}
  \item \emph{reachability}
%  \item \emph{low-level, bitwise arithmetic}
  \end{itemize}
  
  \bigskip
  let us consider some examples
  \begin{itemize}
  \item Bresenham's line drawing algorithm
  \item Dijkstra's shortest path algorithm
%  \item n-queens (backtracking counting of solutions)
  \end{itemize}
\end{frame}

% which theories for program verification

% equality, arithmetic, (arrays)

% we dont use bit vectors, tuples, records, ind. data types 

% no need for machine integers

% would be useful: finite sets, reachability (reflexive transitive
% closure), real / non-linear arith

% not only for academic case studies: for instance, finite sets (and
% even transitive closure) are useful to axiomatize the assigns clause

% inductive data types, induction when SMT solvers used from Coq

% example 1: Bresenham's line drawing

% TODO: figure Bresenham

\begin{frame}\frametitle{Example 1: Bresenham's Line Drawing Algorithm}

draws a discrete line from $(0,0)$ to $(x_2,y_2)$

\begin{why}
logic x2,y2 : int

axiom first_octant : 0 <= y2 <= x2
\end{why}

\bigskip
\texttt{x} varies from 0 to $x_2$ ; \par
at each step, \texttt{y} is 
increased or not, according to the size of \texttt{e}
\begin{why}
parameter x,y,e : int ref
\end{why}
\end{frame}

\begin{frame}\frametitle{Example 1: Bresenham's Line Drawing Algorithm}
\vspace*{-1em}
\begin{why}
let bresenham () =
  x := 0;
  y := 0;
  e := 2 * y2 - x2;
  while !x <= x2 do
    { invariant 0 <= x <= x2 + 1 and 
        e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
        2 * (y2 - x2) <= e <= 2 * y2 }
    (* here we would plot (x,y) *) 
    if !e < 0 then
      e := !e + 2 * y2
    else begin
      y := !y + 1;
      e := !e + 2 * (y2 - x2)
    end;
    x := !x + 1
  done
\end{why}
\end{frame}

\begin{frame}\frametitle{Example 1: Bresenham's Line Drawing Algorithm}

the code only uses linear arithmetic

\bigskip
the specification and thus the proofs require \emph{non-linear arithmetic}

\bigskip
if suffices to add the following axioms
\begin{why}
axiom z_ring_0 : forall a,b,c:int. a * (b+c) = a*b + a*c
axiom z_ring_1 : forall a,b,c:int. (b+c) * a = b*a + c*a
\end{why}

\bigskip
\DEMO
\end{frame}

% example 2: Dijkstra's shortest path

\begin{frame}\frametitle{Example 2: Dijkstra's Shortest Path}
  single-source shortest path in a weighted graph

  \bigskip
  \begin{flushleft}
    $S \leftarrow \emptyset$ \\
    $Q \leftarrow \{src\}$; $d[src] \leftarrow 0$ \\
    while $Q\backslash S$ not empty do \\
    \quad extract $u$ from $Q\backslash S$ with minimal distance $d[u]$ \\
    \quad $S \leftarrow S\cup\{u\}$ \\
    \quad for each vertex $v$ such that $u\stackrel{w}{\rightarrow}v$ \\
    \quad\quad $d[v] \leftarrow \min(d[v], d[u]+w)$ \\
    \quad\quad $Q \leftarrow Q\cup\{v\}$ \\
  \end{flushleft}
\end{frame}

\begin{frame}\frametitle{Example 2: Dijkstra's Shortest Path}
\emph{finite sets} are everywhere in the code/specification:
\begin{itemize}
\item set of vertices $V$
\item set of successors of $u$
\item sets $S$ and $Q$
\end{itemize}

\bigskip
all we need is
\begin{itemize}
\item the empty set $\emptyset$
\item addition $\{x\}\cup s$
\item subtraction $s\backslash \{x\}$
\item membership predicate $x\in s$
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Example 2: Dijkstra's Shortest Path}
\begin{why}
type 'a set

logic set_empty : 'a set
logic set_add : 'a, 'a set -> 'a set
logic set_rmv : 'a, 'a set -> 'a set
logic In : 'a, 'a set -> prop

predicate Is_empty(s : 'a set) = 
  forall x:'a. not In(x, s)

predicate Incl(s1 : 'a set, s2 : 'a set) = 
  forall x:'a. In(x, s1) -> In(x, s2)
\end{why}
\end{frame}

\begin{frame}\frametitle{Example 2: Dijkstra's Shortest Path}
\begin{why}
axiom set_empty_def : 
  Is_empty(set_empty)

axiom set_add_def : 
  forall x:'a. forall y:'a. forall s:'a set. 
  In(x, set_add(y,s)) <-> (x = y or In(x, s))

axiom set_rmv_def :
  forall x:'a. forall y:'a. forall s:'a set. 
  In(x, set_rmv(y,s)) <-> (x <> y and In(x, s))
\end{why}
\end{frame}

\begin{frame}\frametitle{Example 2: Dijkstra's Shortest Path}

termination requires the notion of cardinality

\begin{why}
logic set_card : 'a set -> int

axiom card_nonneg : forall s:'a set. set_card(s) >= 0

axiom card_set_add : 
  forall x:'a. forall s:'a set. 
  not In(x,s) -> set_card(set_add(x,s)) = 1 + set_card(s)

axiom card_set_rmv : 
  forall x:'a. forall s:'a set. 
  In(x,s) -> set_card(s) = 1 + set_card(set_rmv(x, s))

axiom card_Incl :
  forall s1,s2 : 'a set. 
  Incl(s1,s2) -> set_card(s1) <= set_card(s2)
\end{why}
\end{frame}

\begin{frame}\frametitle{Example 2: Dijkstra's Shortest Path}
\begin{why}
while ... do
  { ... variant set_card(V) - set_card(S) }
  ...
  S := set_add u !S;
  ...
  while ... do 
    { ... variant set_card(su) }  
    ...
    su := set_rmv v !su
  done
done
\end{why}
\end{frame}

\begin{frame}\frametitle{Finite Sets}
  a theory of \emph{finite sets} with constant $\emptyset$, operations
  $\{x\}\cup s$, $s\backslash\{x\}$, $\mathsf{card}(s)$ and predicate
  $x\in s$ would be extremely useful (even if incomplete)
\end{frame}

\begin{frame}\frametitle{Example 2: Dijkstra's Shortest Path}
\begin{why}
(* paths *)

logic path : vertex, vertex, int -> prop 

axiom path_nil : 
  forall x:vertex. path(x,x,0)

axiom path_cons : 
  forall x,y,z:vertex. forall d:int. 
  path(x,y,d) -> In(z,g_succ(y)) -> 
  path(x,z,d+weight(y,z))

(* and shortest paths *)

predicate shortest_path(x:vertex, y:vertex, d:int) =
  path(x,y,d) and forall d':int. path(x,y,d') -> d <= d'
\end{why}
\end{frame}

\begin{frame}\frametitle{Example 2: Dijkstra's Shortest Path}
\begin{why}
axiom path_inversion :
  forall src,v:vertex. forall d:int. path(src,v,d) ->
    (v = src and d = 0) or
    (exists v':vertex. 
      path(src,v',d - weight(v',v)) and In(v,g_succ(v')))

(* lemmas requiring induction *)

axiom length_nonneg : 
  forall x,y:vertex. forall d:int. path(x,y,d) -> d >= 0

...
\end{why}
\end{frame}

\begin{frame}\frametitle{Reachability}
  more generally, a theory of \emph{reachability} is often used when
  specifying programs

  \bigskip
  this is simply the \emph{reflexive transitive closure} of some
  relation (requires a some kind of higher-order to be generic)

  \bigskip
  variants:
  \begin{itemize}
  \item paths without repetition
  \item paths with the list of nodes ($path(x,y,l)$)
  \item closure of a functionø
  \item etc.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Conversely}
  sometimes, no need for built-in theories

  \bigskip
  examples
  \begin{itemize}
  \item arrays
  \item machine arithmetic (fixed-size integers)
  \item bitwise arithmetic (low-level bit tricks)
  \end{itemize}
\end{frame}

\begin{frame}\frametitle{Machine Arithmetic}
3 possible models for C (integer) arithmetic in Why
\begin{itemize}
\item exact arithmetic
\item bounded arithmetic (no overflow)
\item modulo arithmetic (faithful to program execution)
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Bounded Arithmetic}
\begin{why}
type int32

logic of_int32: int32 -> int

axiom int32_domain :
 forall x:int32. -2147483648 <= of_int32(x) <= 2147483647

parameter int32_of_int :
  x:int ->
    { -2147483648 <= x <= 2147483647 } 
    int32 
    { of_int32(result) = x }
\end{why}
\end{frame}

\begin{frame}\frametitle{Bounded Arithmetic}
a C operation such as $x+y$ is translated into
\begin{why}
  int32_of_int(of_int32(x) + of_int32(y))
\end{why}
which produces the verification condition
\begin{why}
  -2147483648 <= of_int32(x) + of_int32(y) <= 2147483647
\end{why}

\bigskip
no real need for a built-in theory
\end{frame}


\begin{frame}\frametitle{Modulo Arithmetic}
\begin{why}
type int32
logic of_int32: int32 -> int
axiom int32_domain : ...

logic mod_int32: int -> int

parameter int32_of_int :
  x:int -> { } int32 { of_int32(result) = mod_int32(x) }

axiom mod_int32_id :
  forall x:int.
  -2147483648 <= x <= 2147483647 -> mod_int32(x) = x

axiom mod_int32_def :
  forall x,k:int.
  mod_int32(x) = mod_int32(x + k * 4294967296)
\end{why}
\end{frame}

\begin{frame}\frametitle{Modulo Arithmetic}
in some cases, you may only need
\begin{why}
axiom mod_int32_gt :
  forall x:int. x > 2147483647 -> 
  mod_int32(x) = mod_int32(x - 4294967296)

axiom mod_int32_lt :
  forall x:int. x < -2147483648 -> 
  mod_int32(x) = mod_int32(x + 4294967296)
\end{why}

\bigskip
otherwise, you need
\begin{itemize}
\item either non-linear arithmetic
\item or at a built-in theory of modulo arithmetic
\end{itemize}
\end{frame}

\begin{frame}[fragile]\frametitle{Bitwise Arithmetic}
challenge for \emph{the verified program of the month}:

\bigskip

{\scriptsize
\begin{verbatim}
   t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,(
   c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}
\end{verbatim}}
\end{frame}

\begin{frame}\frametitle{Unobfuscating...}
\begin{c}
int t(int a, int b, int c) {
  int d, e=a&~b&~c, f=1;
  if (a)
    for (f=0; d=e&-e; e-=d)
      f += t(a-d, (b+d)*2, (c+d)/2);
  return f;
}

int main(int q) {
  scanf("%d", &q);
  printf("%d\n", t(~(~0<<q), 0, 0));
}
\end{c}

\bigskip
this program reads an integer $n$ \par
and prints the number of solutions to the $n$-queens problem  
\end{frame}

% TODO: explain n-queens code?

% summary: some theories not needed, axioms are ok (arrays, fixed-size integers)
% other theories whould be useful (non-linear arith, finite sets, reachability)

%%% 3 SMT-lib and SMT-comp

\begin{frame}
  \begin{center}
    \hrulefill\\
    \Large\emph{SMT-lib and SMT-comp}
  \end{center}
\end{frame}

% polymorphism, predicate definitions, triggers, booleans
% how to use built-in theories that exist in *some* provers
% output: needs a standard / counter-examples / hints or proofs

% scalability: 
% selection of relevant hypotheses should be done by provers themselves
% goal-directed proof search

\begin{frame}\frametitle{}
\end{frame}

\begin{frame}
  \begin{center}
    \hrulefill\\
    \Large\emph{conclusion}
  \end{center}
\end{frame}

\begin{frame}\frametitle{Conclusion}
  
\end{frame}

\end{document}


%%% Local Variables: 
%%% compile-command: "make smt08-pp.pdf"
%%% End: 
