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

\usepackage{beamerjcf}
\usepackage{tikz}

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

%\newcommand{\Item}{\bigskip\item}
\newcommand{\DEMO}{\begin{center}\emph{DEMO}\end{center}}
\newcommand{\kw}[1]{{\color{blue}#1}}
\newcommand{\minelt}[1]{\ensuremath{\mathit{min\_elt}(#1)}}

\begin{document}

\title[Why/Krakatoa/Caduceus]{The Why/Krakatoa/Caduceus Platform \\ 
for Deductive Program Verification}
\author[Jean-Christophe Filli\^atre]{Jean-Christophe Filli\^atre}
\institute{CNRS \\ Orsay, France}
%\date{July 6th, 2007}
\date[CORTA 2007]{}

\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 
    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}
  \begin{center}
  \includegraphics[width=0.8\textwidth]{./small-big.pdf}
  \end{center}
\end{frame}

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

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

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

    \begin{itemize}
    \item 
      using Hoare logic / weakest preconditions
      
    \item 
      other similar approaches: static verification (ESC/Java,
      SPEC\#), \par
      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 (Simplify, Yices, Ergo, etc.)
    \item proof assistants (Coq, PVS, Isabelle/HOL, etc.)
    \end{itemize}

  \end{itemize}
\end{frame}

\begin{frame}\frametitle{Platform Overview}
%   \setlength{\unitlength}{0.6pt}\scriptsize
%   \input{./platform}
%  \includegraphics[width=0.8\textwidth]{./platform.png}
  \includegraphics[width=\textwidth]{./platform.pdf}
  % \includegraphics[width=\textwidth]{./platform.png}
\end{frame}

\begin{frame}\frametitle{Outline}
  \begin{enumerate}
  \Item specification languages
    \begin{itemize}
    \item how to formally specify behaviors
    \end{itemize}
  \Item generation of VCs
    \begin{itemize}
    \item models of program execution
    \end{itemize}
  \Item discharging VCs
    \begin{itemize}
    \item multi-prover approach
    \end{itemize}
  \end{enumerate}
\end{frame}

\begin{frame}
  \begin{center}
    \emph{part I} \\
    \hrulefill\\
    \Large\emph{Formally Specifying Pointer Programs}
  \end{center}
\end{frame}

% 1. spec languages
%% JML / ACSL 
%% algebraic specifications using type+logic+axiom
%% n-queens example -> ghost code

\begin{frame}\frametitle{Which language to specify behaviors?}
Java already has a specification language: \emph{JML} (Java Modeling Language)

used in runtime assertion checking tools, ESC/Java, JACK, LOOP, CHASE

\bigskip
JML allows to specify
\begin{itemize}
\item precondition, postcondition and side-effects for methods
\item invariant and variant for loops
\item class invariants
\item model fields (\url{~} ghost code)
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Which language to specify behaviors?}
we designed a similar language for \emph{C programs}, largely inspired
by JML

\bigskip
additional features:
\begin{itemize}
\item pointer arithmetic
\item algebraic models
  \begin{itemize}
  \item any axiomatized theory can be used in specifications
  \item no runtime assertion checking
  \end{itemize}
\item floating-point arithmetic 
  \begin{itemize}
  \item round errors can be specified
  \end{itemize}
\end{itemize}
\end{frame}

% \begin{frame}\frametitle{JML example: Purse.java}
% \begin{java}
% class Purse {
    
%     public int balance;

%     /*@ public invariant balance >= 0; */

%     /*@ public normal_behavior
%       @   requires s >= 0;
%       @   modifiable balance;
%       @   ensures balance == \old(balance)+s;
%       @*/
%     public void credit(int s) {
%       balance += s;
%     }
% \end{java}
% \end{frame}

% \begin{frame}\frametitle{JML example: Purse.java (cont'd)}
% \begin{java}
%     /*@ public behavior
%       @  requires s >= 0;
%       @  modifiable balance;
%       @  ensures 
%       @    s <= \old(balance) && balance == \old(balance)-s;
%       @  signals (NoCreditException) 
%       @    s > \old(balance) && balance == \old(balance);
%       @*/
%     public void withdraw(int s) throws NoCreditException {
%       if (balance >= s) {
%         balance -= s;
%       } else {
%         throw new NoCreditException();
%       }
%     }
% \end{java}
% \end{frame}

\begin{frame}\frametitle{A First 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 (code)}
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}int}~binary\_{}search({\color{darkgreen}int}*~t,~{\color{darkgreen}int}~n,~{\color{darkgreen}int}~v)~\{~\\
~~{\color{darkgreen}int}~l~=~0,~u~=~n-1,~p~=~-1;~\\
~~{\color{kwblue}while}~(l~<=~u~)~\{~\\
~~~~{\color{darkgreen}int}~m~=~(l~+~u)~/~2;~\\
~~~~{\color{kwblue}if}~(t[m]~<~v)~\\
~~~~~~l~=~m~+~1;~\\
~~~~{\color{kwblue}else}~{\color{kwblue}if}~(t[m]~>~v)~\\
~~~~~~u~=~m~-~1;~\\
~~~~{\color{kwblue}else}~\{~\\
~~~~~~p~=~m;~{\color{kwblue}break};~\\
~~~~\}~\\
~~\}~\\
~~{\color{kwblue}return}~p;~\\
\}~\\
\end{flushleft}
\end{frame}


\begin{frame}\frametitle{Binary Search (spec)}
  we want to prove:
  \begin{enumerate}
  \Item absence of runtime error
  \Item termination
  \Item behavioral correctness
  \end{enumerate}
\end{frame}

\begin{frame}\frametitle{Binary Search (spec)}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}/*@~{\color{kwblue}requires}~~\\
~~@~~~n~>=~0~\&{}\&{}~~\\
~~@~~~\textbf{\char'134 valid\_{}range}(t,0,n-1)~\&{}\&{}~\\
~~@~~~\textbf{\char'134 forall}~int~k1,~int~k2;~~\\
~~@~~~~~0~<=~k1~<=~k2~<=~n-1~=>~t[k1]~<=~t[k2]~\\
~~@*/\end{slshape}~\\
{\color{darkgreen}int}~binary\_{}search({\color{darkgreen}int}*~t,~{\color{darkgreen}int}~n,~{\color{darkgreen}int}~v)~\{~\\
~~...~\\
\}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Binary Search (spec)}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}/*@~{\color{kwblue}requires}~~\\
~~@~~~n~>=~0~\&{}\&{}~~\\
~~@~~~\textbf{\char'134 valid\_{}range}(t,0,n-1)~\&{}\&{}~\\
~~@~~~\textbf{\char'134 forall}~int~k1,~int~k2;~~\\
~~@~~~~~0~<=~k1~<=~k2~<=~n-1~=>~t[k1]~<=~t[k2]~\\
~~@~{\color{kwblue}ensures}~\\
~~@~~~(\textbf{\char'134 result}~>=~0~\&{}\&{}~t[\textbf{\char'134 result}]~==~v)~||~\\
~~@~~~(\textbf{\char'134 result}~==~-1~\&{}\&{}~\textbf{\char'134 forall}~int~k;~~\\
~~@~~~~~~~~~~~~~~~~~~~~~~~0~<=~k~<~n~=>~t[k]~!=~v)~\\
~~@*/\end{slshape}~\\
{\color{darkgreen}int}~binary\_{}search({\color{darkgreen}int}*~t,~{\color{darkgreen}int}~n,~{\color{darkgreen}int}~v)~\{~\\
~~...~\\
\}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Binary Search (spec)}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}/*@~{\color{kwblue}requires}~...~\\
~~@~{\color{kwblue}ensures}~~...~\\
~~@*/\end{slshape}~\\
{\color{darkgreen}int}~binary\_{}search({\color{darkgreen}int}*~t,~{\color{darkgreen}int}~n,~{\color{darkgreen}int}~v)~\{~\\
~~{\color{darkgreen}int}~l~=~0,~u~=~n-1,~p~=~-1;~\\
~~\begin{slshape}\color{blue}/*@~{\color{kwblue}variant}~u-l~~\\
~~~~@*/\end{slshape}~\\
~~{\color{kwblue}while}~(l~<=~u~)~\{~\\
~~~~...~\\
~~\}~\\
\}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Binary Search (spec)}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}/*@~{\color{kwblue}requires}~...~\\
~~@~{\color{kwblue}ensures}~~...~\\
~~@*/\end{slshape}~\\
{\color{darkgreen}int}~binary\_{}search({\color{darkgreen}int}*~t,~{\color{darkgreen}int}~n,~{\color{darkgreen}int}~v)~\{~\\
~~{\color{darkgreen}int}~l~=~0,~u~=~n-1,~p~=~-1;~\\
~~\begin{slshape}\color{blue}/*@~{\color{kwblue}invariant}~~\\
~~~~@~~~0~<=~l~\&{}\&{}~u~<=~n-1~\&{}\&{}~p~==~-1~\&{}\&{}~\\
~~~~@~~~\textbf{\char'134 forall}~int~k;~~\\
~~~~@~~~~~0~<=~k~<~n~=>~t[k]~==~v~=>~l~<=~k~<=~u~\\
~~~~@~{\color{kwblue}variant}~u-l~~\\
~~~~@*/\end{slshape}~\\
~~{\color{kwblue}while}~(l~<=~u~)~\{~\\
~~~~...~\\
~~\}~\\
\}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Binary Search (proof)}
\DEMO
\end{frame}

%% ALG. MODELS 

\begin{frame}\frametitle{Algebraic Models}
  in JML, annotations are written using \emph{pure Java code}

  this is mandatory to perform \emph{runtime assertion checking}

  \bigskip\bigskip
  but it is often convenient to introduce \emph{axiomatized theories}
  in order to annotate programs, that is
  \begin{itemize}
  \Item abstract types
  \Item function symbols, w or w/o definitions
  \Item predicates, w or w/o definitions
  \Item axioms
  \end{itemize}
\end{frame}

\begin{frame}\frametitle{Example: Priority Queues}

static data structure for a \emph{priority queue} containing integers

\bigskip
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}void}~clear();~~~~~\begin{slshape}\sffamily\color{darkgreen}//~empties~the~queue\end{slshape}~\\
{\color{darkgreen}void}~push({\color{darkgreen}int}~x);~\begin{slshape}\sffamily\color{darkgreen}//~inserts~a~new~element\end{slshape}~\\
{\color{darkgreen}int}~~max();~~~~~~~\begin{slshape}\sffamily\color{darkgreen}//~returns~the~maximal~element\end{slshape}~\\
{\color{darkgreen}int}~~pop();~~~~~~~\begin{slshape}\sffamily\color{darkgreen}//~removes~and~returns~the~maximal~element\end{slshape}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Bags}
\vspace*{-1em}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}type}~bag~\end{slshape}~\\
\pause~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~bag~empty\_{}bag()\end{slshape}~\\
\pause~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~bag~singleton\_{}bag(int~x)\end{slshape}~\\
\pause~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~bag~union\_{}bag(bag~b1,~bag~b2)\end{slshape}~\\
\pause~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}logic}~bag~add\_{}bag(int~x,~bag~b)~~\\
~~@~~~\{~union\_{}bag(b,~singleton\_{}bag(x))~\}~*/\end{slshape}~\\
\pause~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~int~occ\_{}bag(int~x,~bag~b)\end{slshape}~\\
\pause~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}predicate}~is\_{}max\_{}bag(bag~b,~int~m)~\{~\\
~~@~~~occ\_{}bag(m,~b)~>=~1~\&{}\&{}~\\
~~@~~~\textbf{\char'134 forall}~int~x;~occ\_{}bag(x,b)~>=~1~=>~x~<=~m~~\\
~~@~\}~*/\end{slshape}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Priority Queues (spec)}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~bag~model()\end{slshape}~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}ensures}~model()~==~empty\_{}bag()\end{slshape}~\\
{\color{darkgreen}void}~clear();~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}ensures}~model()~==~add\_{}bag(x,~\textbf{\char'134 old}(model()))\end{slshape}~\\
{\color{darkgreen}void}~push({\color{darkgreen}int}~x);~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}ensures}~is\_{}max\_{}bag(model(),~\textbf{\char'134 result})\end{slshape}~\\
{\color{darkgreen}int}~max();~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}ensures}~~is\_{}max\_{}bag(\textbf{\char'134 old}(model()),~\textbf{\char'134 result})~\&{}\&{}~~\\
~~@~~~~~~~~~~\textbf{\char'134 old}(model())~==~add\_{}bag(\textbf{\char'134 result},~model())~~*/\end{slshape}~\\
{\color{darkgreen}int}~pop();~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Implementing Priority Queues}
  implementation: heap encoded in an array

  \begin{center}
    \includegraphics[width=0.7\textwidth]{./heap.pdf}
  \end{center}
\end{frame}

\begin{frame}\frametitle{Trees}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}type}~tree\end{slshape}~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~tree~Empty()\end{slshape}~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~tree~Node(tree~l,~int~x,~tree~r)\end{slshape}~\\
~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Heaps}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}predicate}~is\_{}heap(tree~t)\end{slshape}~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}axiom}~is\_{}heap\_{}def\_{}1:~is\_{}heap(Empty())\end{slshape}~\\
~\\
...~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Trees and Bags}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~bag~bag\_{}of\_{}tree(tree~t)\end{slshape}~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}axiom}~bag\_{}of\_{}tree\_{}def\_{}1:~\\
~~@~~~bag\_{}of\_{}tree(Empty())~==~empty\_{}bag()~\\
~~@*/\end{slshape}~\\
~\\
...~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Trees and Arrays}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~tree~tree\_{}of\_{}array(int~*t,~int~root,~int~bound)~\end{slshape}~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}axiom}~tree\_{}of\_{}array\_{}def\_{}2:~\\
~~@~~~\textbf{\char'134 forall}~int~*t;~\textbf{\char'134 forall}~int~root;~\textbf{\char'134 forall}~int~bound;~\\
~~@~~~~~0~<=~root~<~bound~=>~~\\
~~@~~~~~tree\_{}of\_{}array(t,~root,~bound)~==~~\\
~~@~~~~~Node(tree\_{}of\_{}array(t,~2*root+1,~bound),~~\\
~~@~~~~~~~~~~t[root],~\\
~~@~~~~~~~~~~tree\_{}of\_{}array(t,~2*root+2,~bound))~\\
~~@*/\end{slshape}~\\
~\\
...~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Priority Queues (spec)}
\begin{flushleft}\ttfamily\parindent 0pt
\#{}define~MAXSIZE~100~\\
~\\
{\color{darkgreen}int}~heap[MAXSIZE];~\\
~\\
{\color{darkgreen}int}~size~=~0;~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}invariant}~size\_{}inv~:~0~<=~size~<~MAXSIZE\end{slshape}~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}invariant}~is\_{}heap:~is\_{}heap(tree\_{}of\_{}array(heap,~0,~size))\end{slshape}~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}logic}~bag~model()~~\\
~~@~~~\{~bag\_{}of\_{}tree(tree\_{}of\_{}array(heap,~0,~size))~\}~*/\end{slshape}~\\
\end{flushleft}
\end{frame}

%% GHOST CODE: N-QUEENS

\begin{frame}[fragile]\frametitle{Another (More Challenging) Example}
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}}

\bigskip

appears on a web page collecting C signature programs 

\bigskip

due to Marcel van Kervinck (author of MSCP, a chess program)
\end{frame}

\begin{frame}\frametitle{Unobfuscating...}
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}int}~t({\color{darkgreen}int}~a,~{\color{darkgreen}int}~b,~{\color{darkgreen}int}~c)~\{~\\
~~{\color{darkgreen}int}~d,~e=a\&{}\~{}b\&{}\~{}c,~f=1;~\\
~~{\color{kwblue}if}~(a)~\\
~~~~{\color{kwblue}for}~(f=0;~d=e\&{}-e;~e-=d)~\\
~~~~~~f~+=~t(a-d,~(b+d)*2,~(c+d)/2);~\\
~~{\color{kwblue}return}~f;~\\
\}~\\
~\\
{\color{darkgreen}int}~main({\color{darkgreen}int}~q)~\{~\\
~~scanf("\%{}d",~\&{}q);~\\
~~printf("\%{}d\ensuremath{\backslash}n",~t(\~{}(\~{}0<<q),~0,~0));~\\
\}~\\
\end{flushleft}

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

\begin{frame}[fragile]
  \frametitle{How does it work?}
  \begin{itemize}
  \item backtracking algorithm (no better way to solve the $n$-queens)
  \item integers used as \emph{sets} (bit vectors)
  \end{itemize}
  \bigskip
  \begin{center}
    \begin{tabular}{r|l}
      integers & sets \\\hline
    \verb!0! & $\emptyset$ \\
   \verb!a&b! & $a\cap b$ \\
       \verb!a+b! & $a\cup b$, \quad when $a\cap b=\emptyset$ \\
       \verb!a-b! & $a\backslash\,b$, \quad when $b\subseteq a$ \\
     \verb!~a! & $\complement a$ \\
     \verb!a&-a! & $\minelt{a}$, \quad when $a\not=\emptyset$ \\
     \verb!~(~0<<n)! & $\{0,1,\dots,n-1\}$ \\
     \verb!a*2! & $\{i+1~|~i\in a\}$, \quad written $S(a)$ \\
     \verb!a/2! & $\{i-1~|~i\in a \land i\not=0\}$, \quad written $P(a)$ \\
    \end{tabular}
  \end{center}
\end{frame}

\font\Chess=chess10
\newcommand{\qw}{\vrule height 1.5em width 0pt{\Chess Q}}
\newcommand{\qb}{\vrule height 1.5em width 0pt{\Chess q}}
\newcommand{\qr}{\vrule height 1.5em width 0pt{\color{red}\Chess q}}
\newcommand{\vide}{\vrule height 1.5em width 0pt\phantom{\Chess q}}
\newcommand{\qm}{\vrule height 1.5em width 0pt\hfil?\hfil}

\begin{frame}
  \frametitle{What $a$, $b$ and $c$ mean}
\only<1>{
  \begin{center}
    \begin{tabular}{|c|c|c|c|c|c|c|c|}
      \hline
      \vide & \vide & \vide & \vide & \qb   & \vide & \vide & \vide \\\hline
      \vide & \vide & \vide & \vide & \vide & \vide & \qb   & \vide \\\hline
      \vide & \vide & \vide & \qb   & \vide & \vide & \vide & \vide \\\hline
      \qm & \qm & \qm & \qm & \qm & \qm & \qm & \qm \\\hline
    \end{tabular}
  \end{center}
\bigskip
\phantom{$a$ = columns to be filled = $11100101_2$}
}
\only<2>{
  \begin{center}
    \begin{tabular}{|c|c|c|c|c|c|c|c|}
      \hline
      \vide & \vide & \vide & \vide & \qb   & \vide & \vide & \vide \\\hline
      \vide & \vide & \vide & \vide & \qw   & \vide & \qb   & \vide \\\hline
      \vide & \vide & \vide & \qb   & \qw   & \vide & \qw   & \vide \\\hline
      \qr   & \qr   & \qr   & \qw   & \qw   & \qr   & \qw   & \qr   \\\hline
    \end{tabular}
  \end{center}
\bigskip
$a$ = columns to be filled = $11100101_2$
}
\only<3>{
  \begin{center}
    \begin{tabular}{|c|c|c|c|c|c|c|c|}
      \hline
      \vide & \vide & \vide & \vide & \qb   & \vide & \vide & \vide \\\hline
      \vide & \vide & \vide & \qw   & \vide & \vide & \qb   & \vide \\\hline
      \vide & \vide & \qw   & \qb   & \vide & \qw   & \vide & \vide \\\hline
      \vide & \qr   & \qr   & \vide & \qr   & \vide & \vide & \vide \\\hline
    \end{tabular}
  \end{center}
\bigskip
$b$ = positions to avoid because of left diagonals = $01101000_2$
}
\only<4>{
  \begin{center}
    \begin{tabular}{|c|c|c|c|c|c|c|c|}
      \hline
      \vide & \vide & \vide & \vide & \qb   & \vide & \vide & \vide \\\hline
      \vide & \vide & \vide & \vide & \vide & \qw   & \qb   & \vide \\\hline
      \vide & \vide & \vide & \qb   & \vide & \vide & \qw   & \qw   \\\hline
      \vide & \vide & \vide & \vide & \qr   & \vide & \vide & \qr   \\\hline
    \end{tabular}
  \end{center}
\bigskip
$c$ = positions to avoid because of right diagonals = $00001001_2$
}
\only<5>{
  \begin{center}
    \begin{tabular}{|c|c|c|c|c|c|c|c|}
      \hline
      \vide & \vide & \vide & \vide & \qb   & \vide & \vide & \vide \\\hline
      \vide & \vide & \vide & \qw   & \qw   & \qw   & \qb   & \vide \\\hline
      \vide & \vide & \qw   & \qb   & \qw   & \qw   & \qw   & \qw   \\\hline
      \qr   & \qw   & \qw   & \qw   & \qw   & \qr   & \qw   & \qw   \\\hline
    \end{tabular}
  \end{center}
\bigskip
$a$\&\~{}$b$\&\~{}$c$ = positions to try = $10000100_2$
}
\end{frame}

\begin{frame}\frametitle{Now it is clear}
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}int}~t({\color{darkgreen}int}~a,~{\color{darkgreen}int}~b,~{\color{darkgreen}int}~c)~\{~\\
~~{\color{darkgreen}int}~d,~e=a\&{}\~{}b\&{}\~{}c,~f=1;~\\
~~{\color{kwblue}if}~(a)~\\
~~~~{\color{kwblue}for}~(f=0;~d=e\&{}-e;~e-=d)~\\
~~~~~~f~+=~t(a-d,~(b+d)*2,~(c+d)/2);~\\
~~{\color{kwblue}return}~f;~\\
\}~\\
~\\
{\color{darkgreen}int}~queens({\color{darkgreen}int}~n)~\{~\\
~~{\color{kwblue}return}~t(\~{}(\~{}0<<n),~0,~0);~\\
\}~\\
\end{flushleft}
\end{frame}


\begin{frame}
  \frametitle{Abstract finite sets}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}type}~iset\end{slshape}~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}predicate}~in\_{}(int~x,~iset~s)\end{slshape}~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}predicate}~included(iset~a,~iset~b)~~\\
~~@~~\{~\textbf{\char'134 forall}~int~i;~in\_{}(i,a)~=>~in\_{}(i,b)~\}~*/\end{slshape}~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~iset~empty()\end{slshape}~\\
~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}axiom}~empty\_{}def~:~\textbf{\char'134 forall}~int~i;~!in\_{}(i,empty())\end{slshape}~\\
~\\
...~~~~~\\
\end{flushleft}

total: \emph{66 lines} of functions, predicates and axioms
\end{frame}

\begin{frame}
  \frametitle{C ints as abstract sets}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~iset~iset(int~x)\end{slshape}~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}axiom}~iset\_{}c\_{}zero~:~\textbf{\char'134 forall}~int~x;~~\\
~~@~~~iset(x)==empty()~<=>~x==0~*/\end{slshape}~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}axiom}~iset\_{}c\_{}min\_{}elt~:~\\
~~@~~~\textbf{\char'134 forall}~int~x;~x~!=~0~=>~~\\
~~@~~~~~iset(x\&{}-x)~==~singleton(min\_{}elt(iset(x)))~*/\end{slshape}~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}axiom}~iset\_{}c\_{}diff~:~\textbf{\char'134 forall}~int~a,~int~b;~~\\
~~@~~~iset(a\&{}\~{}b)~==~diff(iset(a),~iset(b))~*/\end{slshape}~\\
~\\
...~\\
\end{flushleft}

total: \emph{27 lines}
\end{frame}

\begin{frame}
  \frametitle{Termination}
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}int}~t({\color{darkgreen}int}~a,~{\color{darkgreen}int}~b,~{\color{darkgreen}int}~c)\{~\\
~~{\color{darkgreen}int}~d,~e=a\&{}\~{}b\&{}\~{}c,~f=1;~\\
~~{\color{kwblue}if}~(a)~\\
~~~~\begin{slshape}\color{blue}//@~{\color{kwblue}variant}~card(iset(e-d))\end{slshape}~\\
~~~~{\color{kwblue}for}~(f=0;~d=e\&{}-e;~e-=d)~\{~\\
~~~~~~f~+=~t(a-d,(b+d)*2,(c+d)/2);~\\
~~~~\}~\\
~~{\color{kwblue}return}~f;~\\
\}~\\
\end{flushleft}
\bigskip
3 verification conditions, all proved automatically

\bigskip
similarly for the termination of the recursive function: \par
7 verification conditions, all proved automatically

\end{frame}


\begin{frame}
  \frametitle{Soundness}
  how to express that we compute the right number, \par
  since the program is not storing anything, \par 
  not even the current solution?

  \bigskip
  answer: by introducing \emph{ghost code} to perform the missing operations
\end{frame}

\begin{frame}
  \frametitle{Ghost code}
  
  ghost code can be regarded as regular code, as soon as
  \begin{itemize}
  \item ghost code does not modify program data
  \item program code does not access ghost data
  \end{itemize}

  \bigskip
  ghost data is purely logical $\Rightarrow$ ne need to check the validity
  of pointers

\end{frame}

\begin{frame}
  \frametitle{Program instrumented with ghost code}
\small
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~int**~sol;~\end{slshape}~\\
\begin{slshape}\color{blue}//@~int~s;~\end{slshape}~\\
\begin{slshape}\color{blue}//@~int*~col;~~\end{slshape}~\\
\begin{slshape}\color{blue}//@~int~k;~~~~~\end{slshape}~\\
~\\
{\color{darkgreen}int}~t({\color{darkgreen}int}~a,~{\color{darkgreen}int}~b,~{\color{darkgreen}int}~c)~\{~\\
~~{\color{darkgreen}int}~d,~e=a\&{}\~{}b\&{}\~{}c,~f=1;~\\
~~{\color{kwblue}if}~(a)~\\
~~~~{\color{kwblue}for}~(f=0;~d=e\&{}-e;~e-=d)~\{~\\
~~~~~~\begin{slshape}\color{blue}//@~col[k]~=~min\_{}elt(d);~~~~~~~~~~~~~~~~~\end{slshape}~\\
~~~~~~\begin{slshape}\color{blue}//@~k++;~~~~~~~~~~~~~~~~~~~~~~~~\end{slshape}~\\
~~~~~~f~+=~t3(a-d,~(b+d)*2,~(c+d)/2);~\\
~~~~~~\begin{slshape}\color{blue}//@~k--;\end{slshape}~\\
~~~~\}~\\
~~\begin{slshape}\color{blue}//@~{\color{kwblue}else}~\end{slshape}~\\
~~\begin{slshape}\color{blue}//@~~~store\_{}solution();\end{slshape}~\\
~~{\color{kwblue}return}~f;~\\
\}~\\
\end{flushleft}
\end{frame}

\begin{frame}
  \frametitle{Program instrumented with ghost code (cont'd)}
\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}/*@~{\color{kwblue}requires}~solution(col)~\\
~~@~{\color{kwblue}assigns}~~s,~sol[s][0..N()-1]~\\
~~@~{\color{kwblue}ensures}~~s==\textbf{\char'134 old}(s)+1~\&{}\&{}~eq\_{}sol(sol[\textbf{\char'134 old}(s)],~col)~\\
~~@*/\end{slshape}~\\
{\color{darkgreen}void}~store\_{}solution();~\\
~\\
\begin{slshape}\color{blue}/*@~{\color{kwblue}requires}~~\\
~~@~~~n~==~N()~\&{}\&{}~s~==~0~\&{}\&{}~k~==~0~\\
~~@~{\color{kwblue}ensures}~~\\
~~@~~~\textbf{\char'134 result}~==~s~\&{}\&{}~\\
~~@~~~sorted(sol,~0,~s)~\&{}\&{}~\\
~~@~~~\textbf{\char'134 forall}~int*~t;~solution(t)~<=>~~\\
~~@~~~~~~(\textbf{\char'134 exists}~int~i;~0<=i<\textbf{\char'134 result}~\&{}\&{}~eq\_{}sol(t,sol[i]))~\\
~~@*/\end{slshape}~\\
{\color{darkgreen}int}~queens({\color{darkgreen}int}~n)~\{~{\color{kwblue}return}~t(\~{}(\~{}0<<n),~0,~0);~\}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{Finally, we get...}

\emph{256} lines of code and specification

\bigskip
regarding VCs:
\begin{itemize}
\item main function \texttt{queens}: \emph{15} verification conditions
  \begin{itemize}
  \item \emph{all} proved automatically (Simplify, Ergo or Yices)
  \end{itemize}
\item recursive function \texttt{t}: \emph{51} verification conditions
  \begin{itemize}
  \item \emph{42} proved automatically: 41 by Simplify, 37 by Ergo and
    35 by Yices
  \item \emph{9} proved manually using Coq (and Simplify)
  \end{itemize}
\end{itemize}
\end{frame}


% 2. generation of VCs
%% Burstall-Bornat + zones
%% no sep logic
%% example P. Muller

\begin{frame}
  \begin{center}
    \emph{part II} \\
    \hrulefill\\
    \Large\emph{Generating the Verification Conditions}
  \end{center}
\end{frame}

\begin{frame}\frametitle{Generating the Verification Conditions}
  \begin{center}
  \includegraphics[width=0.9\textwidth]{./platform.pdf}
  \end{center}
\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}

\begin{frame}\frametitle{To Pointer Programs to Alias-Free Programs}
naive idea: model the \emph{memory as a big array}

\bigskip
using the theory of arrays
\begin{displaymath}
  \begin{array}{l}
    \mathtt{acc} : \mathtt{mem},\mathtt{int} \rightarrow \mathtt{int} \\
    \mathtt{upd} : \mathtt{mem},\mathtt{int},\mathtt{int}
    \rightarrow \mathtt{mem} \\[1em]
    \forall m\,p\,v, ~
    \mathtt{acc}(\mathtt{upd}(m,p,v), p) = v \\
    \forall m\,p_1\,p_2\,v, ~
    p_1\not=p_2 \Rightarrow \mathtt{acc}(\mathtt{upd}(m,p_1,v), p_2) =
    \mathtt{acc}(m, p_2) \\
  \end{array}
\end{displaymath}
\end{frame}

\begin{frame}\frametitle{Naive Memory Model}
then the C program
\begin{flushleft}\ttfamily\parindent 0pt
~{\color{darkgreen}int}~x;~\\
~{\color{darkgreen}int}~y;~\\
~x~=~0;~\\
~y~=~1;~\\
~\begin{slshape}\color{blue}//@~{\color{kwblue}assert}~x~==~0\end{slshape}~\\
\end{flushleft}

\bigskip
becomes\bigskip

$\begin{array}{l}
  m ~ := ~ \texttt{upd}(m, x, 0); \\
  m ~ := ~ \texttt{upd}(m, y, 1); \\
  \texttt{assert} ~ \texttt{acc}(m, x) = 0
\end{array}$

\bigskip
the verification condition is
\begin{displaymath}
  \texttt{acc}(\texttt{upd}(\texttt{upd}(m, x, 0), y, 0), x) = 0
\end{displaymath}
% requires some reasoning (using $x\not=y$)
\end{frame}

\begin{frame}\frametitle{Memory Model for Pointer Programs}
we use the \emph{component-as-array} model (Burstall-Bornat)

\bigskip
each structure/object field is mapped to a different array

\bigskip
relies on the property \emph{``two different fields cannot be aliased''}

\bigskip\bigskip
strong consequence: prevents pointer casts and unions (a priori)
\end{frame}

\begin{frame}\frametitle{Benefits of the Component-As-Array Model}
\begin{flushleft}\ttfamily\parindent 0pt
~{\color{darkgreen}struct}~S~\{~{\color{darkgreen}int}~x;~{\color{darkgreen}int}~y;~\}~p;~\\
~...~\\
~p.x~=~0;~\\
~p.y~=~1;~\\
~\begin{slshape}\color{blue}//@~{\color{kwblue}assert}~p.x~==~0~~~~\end{slshape}~\\
\end{flushleft}

\bigskip becomes\bigskip

$\begin{array}{l}
  x ~ := ~ \texttt{upd}(x, p, 0); \\
  y ~ := ~ \texttt{upd}(y, p, 1); \\
  \texttt{assert} ~ \texttt{acc}(x, p) = 0
\end{array}$

\bigskip
the verification condition is
\begin{displaymath}
  \texttt{acc}(\texttt{upd}(x, p, 0), p) = 0
\end{displaymath}
\end{frame}

\begin{frame}\frametitle{Component-As-Array Model and Pointer Arithmetic}
\vspace*{-2em}
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}struct}~S~\{~{\color{darkgreen}int}~x;~{\color{darkgreen}short}~y;~{\color{darkgreen}struct}~S~*next;~\}~t[3];~~~~~\\
\end{flushleft}
\bigskip
\begin{center}
  \only<1>{\includegraphics[width=0.8\textwidth]{./bb_model.pdf}}
  \only<2>{\includegraphics[width=0.8\textwidth]{./bb_model_x.pdf}}
\end{center}
\end{frame}

\begin{frame}\frametitle{Separation Analysis}
on top of Burstall-Bornat model, we add some \emph{separation analysis}

\begin{itemize}
\Item each pointer is assigned a \emph{zone}
\Item zones are \emph{unified} when pointers are assigned / compared
\Item functions are \emph{polymorphic} wrt zones
\end{itemize}

\bigskip
similar to ML-type inference

\bigskip
then the component-as-array model is refined according to zones

\bigskip
\textit{Separation Analysis for Deductive Verification} (HAV'07)
\end{frame}

\begin{frame}\frametitle{Separation Analysis}
\vspace*{-2em}
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}struct}~S~\{~{\color{darkgreen}int}~x;~{\color{darkgreen}short}~y;~{\color{darkgreen}struct}~S~*next;~\}~t1[3],~t2[2];~~~~~\\
\end{flushleft}
\bigskip
\begin{center}
  \only<1>{\includegraphics[width=0.8\textwidth]{./bb_model_zones.pdf}}
  \only<2>{\includegraphics[width=0.8\textwidth]{./bb_model_zones_x.pdf}}
\end{center}
\end{frame}

\begin{frame}\frametitle{Example}
little challenge for program verification proposed by P. M\"uller:
\begin{quote}
count the number $n$ of non-zero values in an integer array $t$, \par
then copy these values in a freshly allocated array of size $n$
\end{quote}

\bigskip
\begin{center}
  \begin{tabular}{l|c|c|c|c|c|c|c|c|}
    \cline{2-9}
    \texttt{t} & 2 & 1 & 0 & 4 & 0 & 5 & 3 & 0 
    \\\cline{2-9}\multicolumn{9}{l}{\vspace*{1em}}\\
    \multicolumn{9}{l}{\vspace*{2em}\texttt{count}=5}
    \\\cline{2-6}
    \texttt{u} & 2 & 1 & 4 & 5 & 3 & \multicolumn{3}{l}{}
    \\\cline{2-6}
  \end{tabular}
\end{center}
\end{frame}

\begin{frame}\frametitle{P. M\"uller's Example (code)}
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}void}~m({\color{darkgreen}int}~t[],~{\color{darkgreen}int}~length)~\{~\\
~~{\color{darkgreen}int}~count=0,~i,~*u;~\\
~\\
~~{\color{kwblue}for}~(i=0~;~i~<~length;~i++)~\\
~~~~{\color{kwblue}if}~(t[i]~>~0)~count++;~\\
~\\
~~u~=~({\color{darkgreen}int}~*)calloc(count,sizeof({\color{darkgreen}int}));~\\
~~count~=~0;~\\
~\\
~~{\color{kwblue}for}~(i=0~;~i~<~length;~i++)~\\
~~~~{\color{kwblue}if}~(t[i]~>~0)~u[count++]~=~t[i];~\\
\}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{P. M\"uller's Example (spec)}
\begin{flushleft}\ttfamily\parindent 0pt
{\color{darkgreen}void}~m({\color{darkgreen}int}~t[],~{\color{darkgreen}int}~length)~\{~\\
~~{\color{darkgreen}int}~count=0,~i,~*u;~\\
~~\begin{slshape}\color{blue}//@~{\color{kwblue}invariant}~count~==~num\_{}of\_{}pos(0,i-1,t)~...~\end{slshape}~\\
~~{\color{kwblue}for}~(i=0~;~i~<~length;~i++)~\\
~~~~{\color{kwblue}if}~(t[i]~>~0)~count++;~\\
~~\begin{slshape}\color{blue}//@~{\color{kwblue}assert}~count~==~num\_{}of\_{}pos(0,length-1,t)\end{slshape}~\\
~~u~=~({\color{darkgreen}int}~*)calloc(count,sizeof({\color{darkgreen}int}));~\\
~~count~=~0;~\\
~~\begin{slshape}\color{blue}//@~{\color{kwblue}invariant}~count~==~num\_{}of\_{}pos(0,i-1,t)~...~\end{slshape}~\\
~~{\color{kwblue}for}~(i=0~;~i~<~length;~i++)~\\
~~~~{\color{kwblue}if}~(t[i]~>~0)~u[count++]~=~t[i];~\\
\}~\\
\end{flushleft}
\end{frame}

\begin{frame}\frametitle{P. M\"uller's Example (proof)}

12 verification conditions

\begin{itemize}
\item without separation analysis: 10/12 automatically proved
\item with separation analysis: 12/12 automatically proved
\end{itemize}

\bigskip\bigskip\DEMO
\end{frame}

% 3. discharging VCs
%% Why = polymorphic first-order logic
%% off-the-shelf provers
%% typing issues

\begin{frame}
  \begin{center}
    \emph{part III} \\
    \hrulefill\\
    \Large\emph{Discharging the Verification Conditions}
  \end{center}
\end{frame}

\begin{frame}\frametitle{Which Provers}
we want to use \emph{off-the-shelf provers}, as many as possible

\bigskip
requirements
\begin{itemize}
\item first-order logic
\item equality and arithmetic
\item quantifiers (memory model, user algebraic models)
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Provers Currently Supported}
\emph{automatic decision procedures}
\begin{itemize}
\item provers \textit{a la} Nelson-Oppen 
  \begin{itemize}
  \item Simplify, Yices, Ergo
  \item CVC Lite, CVC3
  \end{itemize}
\item resolution based provers
  \begin{itemize}
  \item harvey, rv-sat
  \item Zenon
  \end{itemize}
\end{itemize}

\bigskip
\emph{interactive proof assistants}
\begin{itemize}
\item Coq, PVS, Isabelle/HOL
\item HOL4, HOL Light, Mizar
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Typing Issues}
verification conditions are expressed in polymorphic first-order logic

\bigskip
need to be \emph{translated} to logics with various type systems:
\begin{itemize}
\item unsorted logic (Simplify, Zenon)
\item simply sorted logic (SMT provers)
\item parametric polymorphism (CVC Lite, PVS)
\item polymorphic logic (Ergo, Coq, Isabelle/HOL)
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Typing Issues}
forgetting types is unsound

\begin{flushleft}\ttfamily\parindent 0pt
\begin{slshape}\color{blue}//@~{\color{kwblue}type}~color\end{slshape}~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~color~black\end{slshape}~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}logic}~color~white\end{slshape}~\\
\begin{slshape}\color{blue}//@~{\color{kwblue}axiom}~color:~\textbf{\char'134 forall}~color~c;~c==white~||~c==black\end{slshape}~\\
\end{flushleft}

\bigskip
\begin{displaymath}
  \forall c,~c=\mathtt{white}\lor c=\mathtt{black}
  ~\vdash~
  \bot
\end{displaymath}
\end{frame}

\begin{frame}\frametitle{Type Encoding}
several type encodings are used
\begin{itemize}
\item monomorphization
  \begin{itemize}
  \item may loop
  \end{itemize}
\item usual encoding ``types-as-predicates''
  \begin{itemize}
  \item does not combine nicely with most provers
  \end{itemize}
\item new encoding with \emph{type-decorated terms}

  %J.-F.~Couchot and S.~Lescuyer \par
  \textit{Handling Polymorphism in Automated Deduction} (CADE 21)
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Trust in Prover Results}
\begin{itemize}
\item some provers apply the de Bruijn principle and thus are \emph{safe}
  \begin{itemize}
  \item Coq, HOL family
  \end{itemize}
\item most provers \emph{have to be trusted}
  \begin{itemize}
  \item Simplify, Yices
  \item PVS, Mizar
  \end{itemize}
\item some provers output \emph{proof traces}
  \begin{itemize}
  \item Ergo, CVC family, Zenon
  \end{itemize}
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Provers Collaboration}
most of the time, we run the various provers \emph{in parallel}, \par
expecting at least one of them to discharge the VC

\bigskip
if not, we turn to interactive theorem provers

\bigskip
\begin{itemize}
\item 
  no real collaboration between automatic provers

\item 
  from Coq or Isabelle, one can call automatic theorem provers
  \begin{itemize}
  \item proofs are checked when available
  \item results are trusted otherwise
  \end{itemize}
\end{itemize}
\end{frame}

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

\begin{frame}\frametitle{Summary}
the Why/Krakatoa/Caduceus platform features
  \begin{itemize}
  \item behavioral specification languages for C and Java programs,
    \par
    at source code level
  \item deductive program verification using original memory models
  \item multi-provers backend (interactive and automatic)
  \end{itemize}

\bigskip
successfully applied on both
\begin{itemize}
\item academic case studies (Schorr-Waite, N-queens, list reversal, etc.)
\item industrial case studies (Gemalto, Dassault Aviation, France Telecom)
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Other Features}
other features not covered in this talk
  \begin{itemize}
  \Item \emph{floating point arithmetic}
  \begin{itemize}
  \item allows to specify rounding and method errors
  \item \textit{Formal Verification of Floating-Point Programs} (ARITH 18)
  \end{itemize}

  \Item \emph{pruning strategies} to help decision procedures on large VCs 
  \end{itemize}
\end{frame}

\begin{frame}\frametitle{Ongoing Work \&{} Future Work}
ongoing work
  \begin{itemize}
  \item ownership: when class/type invariants must hold?
  \item C unions \&{} pointer casts
  \end{itemize}

\bigskip
future work
  \begin{itemize}
  \item verification of ML programs
  \end{itemize}
\end{frame}

\end{document}

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