\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)}}
\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[The Why platform]{The Why Platform \\ 
for Deductive Program Verification}
\author[Jean-Christophe Filli\^atre]{Jean-Christophe Filli\^atre}
\institute{CNRS \\ Orsay, France}
\date{Porto, July 4, 2008}
%\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 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 verification technique
  \Item discharging the verification conditions
  \Item ongoing and future work
  \end{enumerate}
\end{frame}

\begin{frame}
  \begin{center}
    \hrulefill\\
    \Large\emph{overview of the Why platform}
  \end{center}
\end{frame}

\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 
      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 (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{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}{\color{darkgreen}int} binary\_{}search({\color{darkgreen}int}* t, {\color{darkgreen}int} n, {\color{darkgreen}int} v) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} l = 0, u = n-1;~\linebreak
\noindent\hspace*{1.00em}{\color{blue}while} (l <= u ) \{~\linebreak
\noindent\hspace*{2.00em}{\color{darkgreen}int} m = (l + u) / 2;~\linebreak
\noindent\hspace*{2.00em}{\color{blue}if} (t[m] < v)~\linebreak
\noindent\hspace*{3.00em}l = m + 1;~\linebreak
\noindent\hspace*{2.00em}{\color{blue}else} {\color{blue}if} (t[m] > v)~\linebreak
\noindent\hspace*{3.00em}u = m - 1;~\linebreak
\noindent\hspace*{2.00em}{\color{blue}else} ~\linebreak
\noindent\hspace*{3.00em}{\color{blue}return} m;~\linebreak
\noindent\hspace*{1.00em}\}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}return} -1;~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\end{frame}


\begin{frame}\frametitle{Binary Search}
  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: Safety}

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

\bigskip

\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}/*@~requires~n~>=~0~\&{}\&{}~\ensuremath{\backslash}valid\_{}range(t,0,n-1)~*/}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} binary\_{}search({\color{darkgreen}int}* t, {\color{darkgreen}int} n, {\color{darkgreen}int} v) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} l = 0, u = n-1;~\linebreak
\noindent\hspace*{1.00em}\emph{\color{red}/*@~invariant~0~<=~l~\&{}\&{}~u~<=~n-1~*/}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}while} (l <= u ) \{~\linebreak
\noindent\hspace*{2.00em}...~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\DEMO
\end{frame}

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

we add a \emph{variant} to prove termination

\bigskip

\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}/*@~requires~n~>=~0~\&{}\&{}~\ensuremath{\backslash}valid\_{}range(t,0,n-1)~*/}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} binary\_{}search({\color{darkgreen}int}* t, {\color{darkgreen}int} n, {\color{darkgreen}int} v) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} l = 0, u = n-1;~\linebreak
\noindent\hspace*{1.00em}\emph{\color{red}/*@~invariant~0~<=~l~\&{}\&{}~u~<=~n-1~~\linebreak
\noindent\hspace*{2.00em}@~variant~u~-~l~~\linebreak
\noindent\hspace*{2.00em}@*/}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}while} (l <= u ) \{~\linebreak
\noindent\hspace*{2.00em}...~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\DEMO
\end{frame}

\begin{frame}\frametitle{Binary Search: Behavioral Specification}

we add a \emph{postcondition} for the success case

\bigskip

\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}/*@~requires~n~>=~0~\&{}\&{}~\ensuremath{\backslash}valid\_{}range(t,0,n-1)~~\linebreak
\noindent\hspace*{1.00em}@~ensures~~\ensuremath{\backslash}result~>=~0~=>~t[\ensuremath{\backslash}result]~==~v~~\linebreak
\noindent\hspace*{1.00em}@*/}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} binary\_{}search({\color{darkgreen}int}* t, {\color{darkgreen}int} n, {\color{darkgreen}int} v) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} l = 0, u = n-1;~\linebreak
\noindent\hspace*{1.00em}\emph{\color{red}/*@~invariant~0~<=~l~\&{}\&{}~u~<=~n-1~~\linebreak
\noindent\hspace*{2.00em}@~variant~u~-~l~~\linebreak
\noindent\hspace*{2.00em}@*/}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}while} (l <= u ) \{~\linebreak
\noindent\hspace*{2.00em}...~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\DEMO
\end{frame}

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

we add a postcondition for the failure case $\Rightarrow$ we need a
precondition which says that the array is sorted

\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}/*@~requires~~\linebreak
\noindent\hspace*{1.00em}@~~~n~>=~0~\&{}\&{}~\ensuremath{\backslash}valid\_{}range(t,0,n-1)~\&{}\&{}~\linebreak
\noindent\hspace*{1.00em}@~~~\ensuremath{\backslash}forall~int~k1,~int~k2;~~\linebreak
\noindent\hspace*{1.00em}@~~~~~0~<=~k1~<=~k2~<=~n-1~=>~t[k1]~<=~t[k2]~\linebreak
\noindent\hspace*{1.00em}@~ensures~\linebreak
\noindent\hspace*{1.00em}@~~~(\ensuremath{\backslash}result~>=~0~\&{}\&{}~t[\ensuremath{\backslash}result]~==~v)~||~\linebreak
\noindent\hspace*{1.00em}@~~~(\ensuremath{\backslash}result~==~-1~\&{}\&{}~~\linebreak
\noindent\hspace*{1.00em}@~~~~~~\ensuremath{\backslash}forall~int~k;~0~<=~k~<~n~=>~t[k]~!=~v)~\linebreak
\noindent\hspace*{1.00em}@*/}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} binary\_{}search({\color{darkgreen}int}* t, {\color{darkgreen}int} n, {\color{darkgreen}int} v) \{~\linebreak
\noindent\hspace*{1.00em}...~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\end{frame}

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

requires a stronger invariant

\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}{\color{darkgreen}int} binary\_{}search({\color{darkgreen}int}* t, {\color{darkgreen}int} n, {\color{darkgreen}int} v) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} l = 0, u = n-1;~\linebreak
\noindent\hspace*{1.00em}\emph{\color{red}/*@~invariant~~\linebreak
\noindent\hspace*{2.00em}@~~~0~<=~l~\&{}\&{}~u~<=~n-1~\&{}\&{}~~\linebreak
\noindent\hspace*{2.00em}@~~~\ensuremath{\backslash}forall~int~k;~~\linebreak
\noindent\hspace*{2.00em}@~~~~~~0~<=~k~<~n~=>~t[k]~==~v~=>~l~<=~k~<=~u~\linebreak
\noindent\hspace*{2.00em}@~variant~u-l~~\linebreak
\noindent\hspace*{2.00em}@*/}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}while} (l <= u ) \{~\linebreak
\noindent\hspace*{2.00em}...~\linebreak
\noindent\hspace*{1.00em}\}~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\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{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{1.00em}{\color{darkgreen}int} m = (l + u) / 2;
\end{flushleft}%
a possible overflow is signaled; a possible fix is
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{1.00em}{\color{darkgreen}int} m = l + (u - l) / 2;
\end{flushleft}%

\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{Cases Studies so far}
\emph{academic case studies}
\begin{itemize}
\item Schorr-Waite algorithm \cit{SEFM'05}
\item selection sort, insertion sort, heapsort, quicksort
\item Dijkstra's shortest path
\item Bresenham's line drawing
\item Knuth-Morris-Pratt string searching
\item n-queens (backtracking counting of solutions)
\item several MIX programs from \textit{The Art of Computer Programming}
\end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Cases Studies so far}
\emph{industrial case studies}
\begin{itemize}
\Item Java applets 
\begin{itemize}
\item Java Card transactions at Gemalto \cit{N. Rousset, SEFM'06}
  \begin{itemize}
  \item Industrial banking applet Payflex (Banking) - 4600 loc
  \item SIMSave: SIM/Server synchro - 3800 loc
  \item IAS: government security platform - 20\,000 loc
  \end{itemize}
\item Demoney applet provided by Trusted Logic
\item PSE applet provided by Gemalto \cit{AMAST'04}
\end{itemize}
\Item avionics software from Dassault Aviation \cit{T. Hubert, HAV'07}
  \begin{itemize}
  \item embedded C code checked for safety - 70\,000 loc 
  \end{itemize}
\Item undergoing collaboration with CEA, Airbus, France Télécom,
Continental SA, Dassault Aviation
\end{itemize}
\end{frame}

\begin{frame}
  \begin{center}
    \hrulefill\\
    \Large\emph{verification technique}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Problems to Solve}
  we need 
  \begin{enumerate}
  \Item to get VCs from annotated programs
  \begin{itemize}
  \item how to model the memory
  \item what can be shared between C and Java
  \end{itemize}

  \Item to discharge the VCs
  \begin{itemize}
  \item how to use both automatic and interactive theorem provers
  \end{itemize}
  \end{enumerate}

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

\begin{frame}\frametitle{Modeling the memory}

we need to translate pointer programs to alias-free programs

\bigskip

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

\noindent\hspace*{0.50em}struct S \{ {\color{darkgreen}int} x; {\color{darkgreen}int} y; \} p;~\linebreak
\noindent\hspace*{0.50em}...~\linebreak
\noindent\hspace*{0.50em}p.x = 0;~\linebreak
\noindent\hspace*{0.50em}p.y = 1;~\linebreak
\noindent\hspace*{0.50em}\emph{\color{red}//@~assert~p.x~==~0~~~~}\linebreak\end{flushleft}%

becomes\bigskip

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

\bigskip
the verification condition is
\begin{displaymath}
  \texttt{acc}(\texttt{upd}(\texttt{upd}(m, px, 0), py, 1), px) = 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

\noindent\hspace*{0.50em}struct S \{ {\color{darkgreen}int} x; {\color{darkgreen}int} y; \} p;~\linebreak
\noindent\hspace*{0.50em}...~\linebreak
\noindent\hspace*{0.50em}p.x = 0;~\linebreak
\noindent\hspace*{0.50em}p.y = 1;~\linebreak
\noindent\hspace*{0.50em}\emph{\color{red}//@~assert~p.x~==~0~~~~}\linebreak\end{flushleft}%

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

\noindent\hspace*{0.00em}struct S \{ {\color{darkgreen}int} x; short y; 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} \cit{HAV'07}
\end{frame}

\begin{frame}\frametitle{Separation Analysis}
\vspace*{-2em}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}struct S \{ {\color{darkgreen}int} x; short y; 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{n}=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

\noindent\hspace*{0.00em}{\color{darkgreen}void} m({\color{darkgreen}int} t[], {\color{darkgreen}int} length) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} count=0, i, *u;~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}for} (i=0 ; i < length; i++)~\linebreak
\noindent\hspace*{2.00em}{\color{blue}if} (t[i] > 0) count++;~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{1.00em}u = ({\color{darkgreen}int} *)calloc(count,sizeof({\color{darkgreen}int}));~\linebreak
\noindent\hspace*{1.00em}count = 0;~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}for} (i=0 ; i < length; i++)~\linebreak
\noindent\hspace*{2.00em}{\color{blue}if} (t[i] > 0) u[count++] = t[i];~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\end{frame}

\begin{frame}\frametitle{P. M\"uller's Example (spec)}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}{\color{darkgreen}void} m({\color{darkgreen}int} t[], {\color{darkgreen}int} length) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} count=0, i, *u;~\linebreak
\noindent\hspace*{1.00em}\emph{\color{red}//@~invariant~count~==~num\_{}of\_{}pos(0,i-1,t)~...~}\linebreak
\noindent\hspace*{1.00em}{\color{blue}for} (i=0 ; i < length; i++)~\linebreak
\noindent\hspace*{2.00em}{\color{blue}if} (t[i] > 0) count++;~\linebreak
\noindent\hspace*{1.00em}\emph{\color{red}//@~assert~count~==~num\_{}of\_{}pos(0,length-1,t)}\linebreak
\noindent\hspace*{1.00em}u = ({\color{darkgreen}int} *)calloc(count,sizeof({\color{darkgreen}int}));~\linebreak
\noindent\hspace*{1.00em}count = 0;~\linebreak
\noindent\hspace*{1.00em}\emph{\color{red}//@~invariant~count~==~num\_{}of\_{}pos(0,i-1,t)~...~}\linebreak
\noindent\hspace*{1.00em}{\color{blue}for} (i=0 ; i < length; i++)~\linebreak
\noindent\hspace*{2.00em}{\color{blue}if} (t[i] > 0) u[count++] = t[i];~\linebreak
\noindent\hspace*{0.00em}\}
\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}


\begin{frame}
  \begin{center}
    \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 Alt-Ergo \cit{\url{http://alt-ergo.lri.fr/}, SMT'07, SMT'08}
  \item Simplify, Yices, Z3, CVC3
  \end{itemize}
\item resolution based provers
  \begin{itemize}
  \item harvey, rv-sat, 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{Using Several Provers}
  \begin{itemize}
  \item built-in theories vs algebraic models
  \Item typing issues: provers do not implement the same logics
  \Item trust in prover results
  \Item provers collaboration
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Built-in Theories and Algebraic Models}
  some provers implement built-in theories, such as
  \begin{itemize}
  \item purely applicative arrays
  \item real arithmetic
  \item bit vectors
  \item tuples
  \end{itemize}
  in practice, the intersection is limited to linear arithmetic

  \bigskip
  so we \emph{axiomatize} the theory we need and rely on the
  quantifier instantiation capabilities (both risky and incomplete)
\end{frame}

\begin{frame}
  \frametitle{Example 1: Bresenham Line Drawing Algorithm}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//~draw~a~line~from~(0,0)~to~(x2,y2)~assuming~0~<=~y2~<=~x2}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}void} bresenham() \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} x = 0;~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} y = 0;~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} e = 2 * y2 - x2;~\linebreak
\noindent\hspace*{1.00em}{\color{blue}for} (x = 0; x <= x2; x++) \{~\linebreak
\noindent\hspace*{2.00em}\emph{\color{red}//~plot~(x,y)~at~this~point}\linebreak
\noindent\hspace*{2.00em}{\color{blue}if} (e < 0)~\linebreak
\noindent\hspace*{3.00em}e += 2 * y2;~\linebreak
\noindent\hspace*{2.00em}{\color{blue}else} \{~\linebreak
\noindent\hspace*{3.00em}y++;~\linebreak
\noindent\hspace*{3.00em}e += 2 * (y2 - x2);~\linebreak
\noindent\hspace*{2.00em}\}~\linebreak
\noindent\hspace*{1.00em}\}~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\end{frame}

\begin{frame}
  \frametitle{Example 1: Bresenham Line Drawing Algorithm}
  the code only uses additions, \par
  but the loop invariant requires \emph{non-linear} arithmetic
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{1.00em}\emph{\color{red}/*@~invariant~~\linebreak
\noindent\hspace*{2.00em}@~~~0~<=~x~<=~x2~+~1~\&{}\&{}~~\linebreak
\noindent\hspace*{2.00em}@~~~e~==~2~*~(x~+~1)~*~y2~-~(2~*~y~+~1)~*~x2~\&{}\&{}~\linebreak
\noindent\hspace*{2.00em}@~~~2~*~(y2~-~x2)~<=~e~<=~2~*~y2~\linebreak
\noindent\hspace*{2.00em}@*/}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}for} (x = 0; x <= x2; x++) \{~\linebreak
\noindent\hspace*{2.00em}\emph{\color{red}//~plot~(x,y)~at~this~point}\linebreak
\noindent\hspace*{2.00em}...
\end{flushleft}%
\end{frame}

\begin{frame}
  \frametitle{Example 1: Bresenham Line Drawing Algorithm}
we can help the provers with the following axioms
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}/*@~axiom~distr\_{}left~:~~\linebreak
\noindent\hspace*{1.00em}@~~~\ensuremath{\backslash}forall~int~a,~int~b,~int~c;~a~*~(b+c)~==~a*b~+~a*c~\linebreak
\noindent\hspace*{1.00em}@*/}~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~axiom~distr\_{}right~:~~\linebreak
\noindent\hspace*{1.00em}@~~~\ensuremath{\backslash}forall~int~a,~int~b,~int~c;~(b+c)~*~a~==~b*a~+~c*a~\linebreak
\noindent\hspace*{1.00em}@*/}
\end{flushleft}%
\DEMO
\end{frame}

\begin{frame}
  \frametitle{Example 2: Counting Bits}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}{\color{darkgreen}int} count\_{}bits({\color{darkgreen}int} x) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} d, c;~\linebreak
\noindent\hspace*{1.00em}{\color{blue}for} (c = 0; d = x\&{}-x; x -= d) c++;~\linebreak
\noindent\hspace*{1.00em}{\color{blue}return} c;~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%

\bigskip
\texttt{x\&-x} extracts the least significant bit of \texttt{x}
\end{frame}

\begin{frame}
  \frametitle{Example 2: Counting Bits}
we introduce a function symbol for the number of bits
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~int~nbits(int~x)}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~ensures~\ensuremath{\backslash}result~==~nbits(x)~*/}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} count\_{}bits({\color{darkgreen}int} x) \{~\linebreak
\noindent\hspace*{1.00em}{\color{darkgreen}int} d, c;~\linebreak
\noindent\hspace*{1.00em}\emph{\color{red}/*@~invariant~c~+~nbits(x)~==~nbits(\ensuremath{\backslash}at(x,init))~\linebreak
\noindent\hspace*{2.00em}@~variant~~~nbits(x)~\linebreak
\noindent\hspace*{2.00em}@*/}~\linebreak
\noindent\hspace*{1.00em}{\color{blue}for} (c = 0; d = x\&{}-x; x -= d) c++;~\linebreak
\noindent\hspace*{1.00em}{\color{blue}return} c;~\linebreak
\noindent\hspace*{0.00em}\}
\end{flushleft}%
\end{frame}

\begin{frame}
  \frametitle{Example 2: Counting Bits}
  then we axiomatize \emph{\texttt{nbits}}:
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~axiom~nbits\_{}nonneg~:~\ensuremath{\backslash}forall~int~x;~nbits(x)~>=~0}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~axiom~nbits\_{}zero~:~nbits(0)~==~0}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~axiom~lowest\_{}bit\_{}zero~:~\linebreak
\noindent\hspace*{1.00em}@~~~\ensuremath{\backslash}forall~int~x;~(x\&{}-x)~==~0~<=>~x~==~0~\linebreak
\noindent\hspace*{1.00em}@*/}~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~axiom~remove\_{}one\_{}bit~:~\linebreak
\noindent\hspace*{1.00em}@~~~~\ensuremath{\backslash}forall~int~x;~~\linebreak
\noindent\hspace*{1.00em}@~~~~~~~x~!=~0~=>~nbits(x~-~(x\&{}-x))~==~nbits(x)~-~1~\linebreak
\noindent\hspace*{1.00em}@*/}
\end{flushleft}%
\end{frame}

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

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

\bigskip
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}{\color{darkgreen}void} clear();     \emph{\color{red}//~empties~the~queue}\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}void} push({\color{darkgreen}int} x); \emph{\color{red}//~inserts~a~new~element}\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int}  max();       \emph{\color{red}//~returns~the~maximal~element}\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int}  pop();       \emph{\color{red}//~removes~and~returns~the~maximal~element}\linebreak\end{flushleft}%
\end{frame}

\begin{frame}\frametitle{Example 3: Priority Queues}
\vspace*{-1em}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~type~bag~}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~bag~empty\_{}bag()}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~bag~singleton\_{}bag(int~x)}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~bag~union\_{}bag(bag~b1,~bag~b2)}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~logic~bag~add\_{}bag(int~x,~bag~b)~~\linebreak
\noindent\hspace*{1.00em}@~~~\{~union\_{}bag(b,~singleton\_{}bag(x))~\}~*/}~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~int~occ\_{}bag(int~x,~bag~b)}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~predicate~is\_{}max\_{}bag(bag~b,~int~m)~\{~\linebreak
\noindent\hspace*{1.00em}@~~~occ\_{}bag(m,~b)~>=~1~\&{}\&{}~\linebreak
\noindent\hspace*{1.00em}@~~~\ensuremath{\backslash}forall~int~x;~occ\_{}bag(x,b)~>=~1~=>~x~<=~m~~\linebreak
\noindent\hspace*{1.00em}@~\}~*/}
\end{flushleft}%
\end{frame}

\begin{frame}\frametitle{Example 3: Priority Queues}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~bag~model()}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~ensures~model()~==~empty\_{}bag()}\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}void} clear();~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~ensures~model()~==~add\_{}bag(x,~\ensuremath{\backslash}old(model()))}\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}void} push({\color{darkgreen}int} x);~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~ensures~is\_{}max\_{}bag(model(),~\ensuremath{\backslash}result)}\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} max();~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~ensures~~is\_{}max\_{}bag(\ensuremath{\backslash}old(model()),~\ensuremath{\backslash}result)~\&{}\&{}~~\linebreak
\noindent\hspace*{1.00em}@~~~~~~~~~~\ensuremath{\backslash}old(model())~==~add\_{}bag(\ensuremath{\backslash}result,~model())~~*/}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} pop();
\end{flushleft}%
\end{frame}

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

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

\begin{frame}\frametitle{Example 3: Priority Queues}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~type~tree}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~tree~Empty()}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~tree~Node(tree~l,~int~x,~tree~r)}\linebreak
\noindent\hspace*{0.00em}
\end{flushleft}%
\end{frame}

\begin{frame}\frametitle{Example 3: Priority Queues}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~predicate~is\_{}heap(tree~t)}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~axiom~is\_{}heap\_{}def\_{}1:~is\_{}heap(Empty())}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}...
\end{flushleft}%
\end{frame}

\begin{frame}\frametitle{Example 3: Priority Queues}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~bag~bag\_{}of\_{}tree(tree~t)}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~axiom~bag\_{}of\_{}tree\_{}def\_{}1:~\linebreak
\noindent\hspace*{1.00em}@~~~bag\_{}of\_{}tree(Empty())~==~empty\_{}bag()~\linebreak
\noindent\hspace*{1.00em}@*/}~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}...
\end{flushleft}%
\end{frame}

\begin{frame}\frametitle{Example 3: Priority Queues}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~tree~tree\_{}of\_{}array(int~*t,~int~root,~int~bound)~}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~axiom~tree\_{}of\_{}array\_{}def\_{}2:~\linebreak
\noindent\hspace*{1.00em}@~~~\ensuremath{\backslash}forall~int~*t;~\ensuremath{\backslash}forall~int~root;~\ensuremath{\backslash}forall~int~bound;~\linebreak
\noindent\hspace*{1.00em}@~~~~~0~<=~root~<~bound~=>~~\linebreak
\noindent\hspace*{1.00em}@~~~~~tree\_{}of\_{}array(t,~root,~bound)~==~~\linebreak
\noindent\hspace*{1.00em}@~~~~~Node(tree\_{}of\_{}array(t,~2*root+1,~bound),~~\linebreak
\noindent\hspace*{1.00em}@~~~~~~~~~~t[root],~\linebreak
\noindent\hspace*{1.00em}@~~~~~~~~~~tree\_{}of\_{}array(t,~2*root+2,~bound))~\linebreak
\noindent\hspace*{1.00em}@*/}~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}...
\end{flushleft}%
\end{frame}

\begin{frame}\frametitle{Example 3: Priority Queues}
\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\#{}define MAXSIZE 100~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} heap[MAXSIZE];~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}{\color{darkgreen}int} size = 0;~\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~invariant~size\_{}inv~:~0~<=~size~<~MAXSIZE}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~invariant~is\_{}heap:~is\_{}heap(tree\_{}of\_{}array(heap,~0,~size))}\linebreak
\noindent\hspace*{0.00em}~\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}/*@~logic~bag~model()~~\linebreak
\noindent\hspace*{1.00em}@~~~\{~bag\_{}of\_{}tree(tree\_{}of\_{}array(heap,~0,~size))~\}~*/}
\end{flushleft}%
\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 (Alt-Ergo, Coq, Isabelle/HOL)
\end{itemize}

\end{frame}

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

\begin{flushleft}\ttfamily\parindent 0pt

\noindent\hspace*{0.00em}\emph{\color{red}//@~type~color}\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~color~black}\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~logic~color~white}\linebreak
\noindent\hspace*{0.00em}\emph{\color{red}//@~axiom~color:~\ensuremath{\backslash}forall~color~c;~c==white~||~c==black}\linebreak\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} \cit{CADE'07}
\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 Alt-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 VCs

\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, ongoing and future work}
  \end{center}
\end{frame}

\begin{frame}\frametitle{Summary}
the Why 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
\item industrial case studies
\end{itemize}

\bigskip
\emph{free software, at \url{http://why.lri.fr/}}
\end{frame}

\begin{frame}\frametitle{Ongoing Work}
  \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} \cit{ARITH'07}
  \item mostly interactive proof (currently Coq, eventually PVS)
  \end{itemize}

  \Item \emph{ownership} 
  \begin{itemize}
  \item when class/type invariants must hold?
  \end{itemize}

  \Item \emph{automatic generation of loop invariants and preconditions} 
  \begin{itemize}
  \item using abstract interpretation techniques \cit{HAV'07}
  \end{itemize}

  \Item \emph{Eclipse plugin (C and Java)}

  \Item \emph{selection of relevant hypotheses} \cit{FTP'07}
  \begin{itemize}
  \item in Why, in Alt-Ergo
  \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}\frametitle{The Future: Frama-C}
  
  \begin{itemize}
  \item more realistic C fragment (unions \&{} pointer casts,
    \texttt{goto}'s, etc.)

  \Item 
    more ambitious specification language
    \begin{center}
      \textit{ACSL: ANSI/ISO C Specification Language}
    \end{center}

  \Item combination of deductive verification and abstract interpretation
  \end{itemize}

  \begin{center}
    see \emph{\url{http://frama-c.cea.fr/}}
  \end{center}

\end{frame}

\end{document}


%%% Local Variables: 
%%% compile-command: "make porto-4-juil-2008-pp.pdf"
%%% End: 
