\documentclass{beamer}

\mode<presentation>
{
  \usetheme[hideothersubsections]{Hannover}
%  \usetheme{Frankfurt}
  \setbeamercovered{transparent}
}

%\usepackage{tikz}
\usepackage{times}

\definecolor{darkgreen}{rgb}{0, 0.5, 0}

\def\bs{\char'134}
\def\numof{\char'134 num\_of}
\newcommand{\pointer}{\texttt{ pointer}}
\newcommand{\memory}{\texttt{ memory}}
\newcommand{\ra}{\ensuremath{\rightarrow}}
\newcommand{\emphc}[1]{\emph{\color{red}#1}}
\newcommand{\ttc}[1]{\texttt{\color{blue}#1}}
\newcommand{\mc}[1]{\ensuremath{\color{darkgreen}#1}}
\newcommand{\cit}[1]{{\color{blue}[#1]}}

\begin{document}
\logo{\pgfuseimage{inriafuturslogo}}

\title[Why\\Krakatoa\\Caduceus]{The Why/Krakatoa/Caduceus Platform \\ for Deductive Program
  Verification}
\author[]{Jean-Christophe Filli\^atre \and Claude March\'e\\
ProVal group - {\color{blue}\url{http://proval.lri.fr}}\\[5mm]
{\footnotesize INRIA-Futurs \& 
LRI, CNRS \& 
Universit\'e Paris-Sud 11: Orsay, France} }

\date{July 4th, 2007}
\begin{frame}
  \titlepage
\pgfimage[height=6mm]{inriafuturslogoshort}\hfill
\pgfimage[height=10mm]{lrilogo}\hfill
\pgfimage[height=8mm]{cnrs-logo}\hfill
\pgfimage[height=8mm]{upsudlogo}

\end{frame}

% \begin{frame}
%   \frametitle{Outline}
%   \tableofcontents
% \end{frame}

% \AtBeginSection[]{
%   \begin{frame}
%     \frametitle{Outline}
%     \tableofcontents[currentsection]
%   \end{frame}
% }

\section{Overview}

\begin{frame}
  \frametitle{The Why/Krakatoa/Caduceus platform}

  
  \begin{itemize}
  \item An environment for proving
    behavioral properties of C and Java source code

  \item Developed in the INRIA ProVal research group

  \item Pure research goal: experimentation of new techniques

  \item Applied goal: case studies on industrial code (Gemalto,
    Dassault Aviation, France Telecom)

 \end{itemize}

 \begin{center}\bfseries
   \textcolor{red}{\url{http://why.lri.fr/}}
 \end{center}

\end{frame}

\begin{frame}
  \frametitle{Originality: versatility}

\begin{itemize}
\item Kernel: the Why tool
  \begin{itemize}
  \item \emphc{Verification Conditions} (VCs) generator\\
    (weakest precondition calculus, quite close to ESC/Java, Spec\#, etc.)
  \item Specific input language:
    \begin{itemize}
    \item designed for deductive verification
    \item behaviors specified in first-order logic
    \end{itemize}
  \end{itemize}
\item Multi-language input
\item Multi-prover output
\end{itemize}

\end{frame}

\begin{frame}
  \frametitle{Platform architecture}

\pgfimage[width=\textwidth]{platform2}

\end{frame}

\begin{frame}
  \frametitle{ProVal group activities}

Three main activities:
  \begin{itemize}
  \item Specification methods/specification languages:
    \begin{itemize}
    \item how to formally specify behaviors
    \item spec. languages largely inspired by JML
    \end{itemize}
  \item Generation of VCs:
    \begin{itemize}
    \item models of program execution \cit{March\'e, Paulin, TPHOLs
        05}, \cit{Filliatre, March\'e, ICFEM 04} 
    \item static analyses (e.g. memory separation~\cit{Hubert, March\'e,
    HAV 07}
    \item Java Card transactions~\cit{March\'e, Rousset, SEFM 06}
    \item floating-point arithmetic~\cit{Boldo, Filli\^atre, ARITH 07}.
    \end{itemize}
  \item Discharging VCs: 
    \begin{itemize}
    \item multi-prover approach, encodings of polymorphic
      sorts~\cit{Couchot, Lescuyer, CADE 07}
    \item cooperation automatic provers/proof assistants
    \end{itemize}
  \end{itemize}

\end{frame}

\section{Example}

\begin{frame}
  \frametitle{Example: Binary search}

\input{bsearch1.c.pp}

\end{frame}

\begin{frame}
  \frametitle{Behavioral specification}

\input{bsearch2.c.pp}

\end{frame}

\begin{frame}
  \frametitle{Loop annotations}

\input{bsearch3.c.pp}

\end{frame}

\begin{frame}
  \frametitle{Remaining unsolved VC}

  \begin{itemize}
  \item In statement \input{bsearch4.c.pp} a possible arithmetic
    overflow is signaled

  \item Fix: replace by \input{bsearch5.c.pp}
  \end{itemize}
\end{frame}

\section{Conclusions, future work}

\begin{frame}
  \frametitle{Conclusions, future work}

Several case studies have been conducted:
\begin{itemize}
\item Java Card applets provided by Gemalto~\cit{Jacobs, March\'e,
    Rauch, AMAST 04}, Trusted Logic
\item Schorr-Waite graph-marking algorithm~\cit{Hubert, March\'e, SEFM
    05}
\item Avionics embedded code, provided by Dassault Aviation
\end{itemize}

Some future work:
\begin{itemize}
\item Higher-level modeling, refinement
\item Automatic generation of annotations
\item Long term perspective: build libraries of verified software
\end{itemize}

\end{frame}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: t
%%% End: 
