\documentclass[a4]{seminar}

%\usepackage{talkadvi}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{pstricks}
\usepackage{pst-node}
\usepackage{color}
\usepackage{alltt}
\usepackage{url}

%\usepackage{pslatex}

\newrgbcolor{krakcolor}{0 0.6 0.2}
\newrgbcolor{whycolor}{0 0.5 1}
\newrgbcolor{coqcolor}{1 0.5 0}
\newrgbcolor{lightgrey}{0.7 0.7 0.7}
\newrgbcolor{lightred}{1 0.8 0.6}
\newrgbcolor{lightgreen}{0.6 1 0.8}
\newrgbcolor{darkgreen}{0 0.6 0}
\definecolor{royalblue}{rgb}{0.25,0.41,0.88}
\definecolor{orange}{rgb}{1.00,0.27,0.00}

\newcommand{\ra}{\rightarrow}
\newcommand{\lra}{\leftrightarrow}
\newcommand{\bs}{\char'134}
\newcommand{\result}{\bs{}result}
\newcommand{\old}{\bs{}old}
\newcommand{\valid}{\bs{}valid}
\newcommand{\Caduceus}{Caduceus}
\newcommand{\Why}{Why}
\newcommand{\tint}{\texttt{int}}
\newcommand{\tpointer}{\texttt{pointer}}
\newcommand{\talloctable}{\texttt{alloc\_table}}
\newcommand{\tmemory}{\texttt{memory}}
\newcommand{\acc}{\texttt{acc}}
\newcommand{\loc}{\texttt{assign\_loc}}
\newcommand{\assigns}{\texttt{assigns}}
\newcommand{\unchanged}{\texttt{unchanged}}
\newcommand{\nothingloc}{\texttt{nothing\_loc}}
\newcommand{\pointerloc}{\texttt{pointer\_loc}}
\newcommand{\rangeloc}{\texttt{range\_loc}}
\newcommand{\allloc}{\texttt{all\_loc}}
\newcommand{\unionloc}{\texttt{union\_loc}}

%for printing
%\usepackage[ignore]{advi}
%\renewcommand{\sliderightmargin}{0mm}
%\renewcommand{\slideleftmargin}{0mm}
%\renewcommand{\slidetopmargin}{-15mm}
%\renewcommand{\slidebottommargin}{0mm}
%\usepackage{palatino}
% for advi view
\usepackage{advi}
\renewcommand{\sliderightmargin}{-25mm}
\renewcommand{\slideleftmargin}{0mm}
\renewcommand{\slidetopmargin}{15mm}
\renewcommand{\slidebottommargin}{0mm}

% pour definir les entetes
\def\myfooter{\vbox to 0em{\vbox to 1.10\vsize {\vfill\normalfont\tiny
{\textcolor{black}{~~~ICFEM'04 --- November 10th, 2004 \hfill \thepage/\ref{lastpage}}}}
\vss}}


\slideframe{none}
\pagestyle{empty}

\def\title#1{%
\myfooter
\unitlength=0.01\textwidth
\textcolor{orange}{\begin{picture}(100,2)
\put(0,0){\line(1,0){100}}
\put(0,2){\makebox{\bfseries\large #1}}
\end{picture}}
\vfill
}

\begin{document}
\sffamily
\parindent=0mm

\begin{slide}
~\vfill
\begin{center}
  \textcolor{red}{\rule{\linewidth}{0.1em}} \\[0.7em]
  \textcolor{red}{\Large\bfseries 
          Multi-Prover Verification of C Programs} \\
  \textcolor{red}{\rule{\linewidth}{0.1em}} \\[2em]
  \textcolor{royalblue}{\large Jean-Christophe Filliâtre, Claude Marché}
 \\[3em]
  \textcolor{orange}{{\large Université Paris Sud}}
\end{center}
\vfill\vfill
\end{slide}


\begin{slide}
\title{Introduction and Motivations}

We propose 
\begin{itemize}
\item a new language for specifying C programs (annotations into
  comments, à la JML)
\item a new approach for the verification of such annotated programs
\item an implementation: the \Caduceus{} tool
% freely available at
%\textcolor{orange}{\url{http://why.lri.fr/caduceus}}
\end{itemize}

\vfill 

\Caduceus{} is currently under experimentation on industrial
embedded programs:
\begin{itemize}
\item Axalto company (smart cards)
\item Dassault Aviation company (avionics)
\end{itemize}

\vfill
\end{slide}


\begin{slide}
\title{Overview of the talk}

\begin{enumerate}
\item Usage of our tool illustrated on examples
  \begin{enumerate}
  \item a simple character queue
  \item in-place linked-list reversal
  \item the Schorr-Waite graph marking algorithm
    \bigskip
  \end{enumerate}
\item Underlying verification technique
\item Limitations, perspectives
\end{enumerate}
\vfill\vfill
\end{slide}



\begin{slide}
\title{Example: character queue as circular array}

%We start with a very simple C program implementing a character queue
%within a circular array. The queue is a global structure \texttt{q}
%The array \texttt{q.contents} contains the queue elements
%stored from index \texttt{q.first} included to index \texttt{q.last} excluded.
%\texttt{q.length} is the length of \texttt{q.contents}, that is the
%maximal capacity of the queue. The boolean fields \texttt{q.empty} and
%\texttt{q.full} indicate whether the queue is empty or full respectively.

\begin{center}
\unitlength=0.5mm
  \psset{unit=\unitlength}
\begin{picture}(100,10)
\pspolygon[linestyle=none,fillstyle=solid,fillcolor=green](20,0)(70,0)(70,10)(20,10)
\multiput(0,0)(0,10){2}{\line(1,0){100}}
\multiput(0,0)(10,0){11}{\line(0,1){10}}
\put(5,17){\makebox(0,0)[c]{\small $0$}}
\put(5,13){\makebox(0,0)[c]{\tiny $\downarrow$}}
\put(95,17){\makebox(0,0)[c]{\small $\texttt{length}-1$}}
\put(95,13){\makebox(0,0)[c]{\tiny $\downarrow$}}
\put(25,-7){\makebox(0,0)[c]{\small \texttt{first}}}
\put(25,-3){\makebox(0,0)[c]{\tiny $\uparrow$}}
\put(75,-7){\makebox(0,0)[c]{\small \texttt{last}}}
\put(75,-3){\makebox(0,0)[c]{\tiny $\uparrow$}}
\end{picture}
\end{center}

\begin{small}
\begin{alltt}
struct queue \{ 
  char contents[];
  int length;
  int first, last;
  unsigned int empty, full :1;
\} q;\adviwait
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
/*@ invariant q_invariant : 
  @   \valid_range(q.contents, 0, q.length-1) &&
  @   0 <= q.first < q.length &&
  @   0 <= q.last < q.length
  @*/
\end{alltt}\end{minipage}}
\end{alltt}
\end{small}
% \vfill
\end{slide}

\begin{slide}
\title{Example continued: specifying functions}

\begin{flushleft}\small
\begin{alltt}
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
/*@ requires !q.full
  @ assigns  q.empty, q.full, q.last, q.contents[q.last]
  @ ensures  !q.empty && q.contents[\old(q.last)] == c
  @*/
\end{alltt}\end{minipage}}
void push(char c); 

\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
/*@ requires !q.empty
  @ assigns q.empty, q.full, q.first
  @ ensures !q.full && \result == q.contents[\old(q.first)]
  @*/
\end{alltt}\end{minipage}}
char pop();
\end{alltt}
\end{flushleft}
\vfill
\end{slide}

\begin{slide}
\title{Example continued: body for \texttt{push} function}

\begin{small}
\begin{alltt}
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
/*@ requires !q.full
  @ assigns  q.empty, q.full, q.last, q.contents[q.last]
  @ ensures  !q.empty && q.contents[\old(q.last)] == c
  @*/
\end{alltt}\end{minipage}}
void push(char c) \{
  q.contents[q.last++] = c;     \textcolor{blue}{// insert 'c' in the queue}
  if (q.last == q.length) 
        q.last = 0;             \textcolor{blue}{// wrap if needed}
  q.empty = 0;                  \textcolor{blue}{// queue is not empty}
  q.full = (q.first == q.last); \textcolor{blue}{// queue is full if}
                                \textcolor{blue}{// 'last' reaches 'first'}
\}
\end{alltt}
\end{small}
\vfill
\end{slide}


\begin{slide}
  \title{Multi-prover architecture}

\vspace*{1em}
\begin{center}
  \unitlength=4mm
  \psset{unit=\unitlength,colsep=1,shortput=nab,%
    arrows=->,labelsep=3pt,nodesep=3pt,%
    arrowlength=1,arrowinset=0.2,angleA=-90,angleB=90,arm=8mm,linearc=3mm}
  \begin{picture}(20,10)
   \rput(10,10){\rnode{c}{\psframebox[linestyle=none,fillstyle=solid,fillcolor=lightgrey]{Annotated C program}}}
   \rput(10,7){\rnode{caduceus}{\psframebox[fillstyle=solid,fillcolor=lightred]{~~{\large \Caduceus}~~}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{c}{caduceus} 
   \rput(-2,2){\rnode{coq}{\psframebox[fillstyle=solid,fillcolor=cyan]{~~Coq~~}}}
   \ncangle[linecolor=red,linewidth=4pt]{->}{caduceus}{coq}
   \rput(4,2){\rnode{pvs}{\psframebox[fillstyle=solid,fillcolor=cyan]{~~PVS~~}}}
   \ncangle[linecolor=red,linewidth=4pt]{->}{caduceus}{pvs}
   \rput(10,2){\rnode{simplify}{\psframebox[fillstyle=solid,fillcolor=yellow]{~~Simplify~~}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{caduceus}{simplify}
   \rput(16,2){\rnode{cvc}{\psframebox[fillstyle=solid,fillcolor=yellow]{~~CVC Lite~~}}}
   \ncangle[linecolor=red,linewidth=4pt]{->}{caduceus}{cvc}
   \rput(22,2){\rnode{harvey}{\psframebox[fillstyle=solid,fillcolor=yellow]{~~haRVey~~}}}
   \ncangle[linecolor=red,linewidth=4pt]{->}{caduceus}{harvey}
%   \rput(15,6){\colorbox{white}{Verification conditions}} 
   \rput(10,0){\psframebox[linestyle=none,fillstyle=solid,fillcolor=lightgrey]{Verification conditions}} 
\end{picture}
\end{center}
\vfill
\end{slide}

\begin{slide}
  \title{Example continued: certification of \texttt{push} function}

\Caduceus{} produces 3 verification conditions expressing that
\begin{itemize}
\item the code of \texttt{push} contains no unallocated pointer dereference
  (e.g. assignment of \textcolor{blue}{\texttt{q.contents[q.last++]}}
  is valid).  
\item the postcondition and the \textcolor{blue}{\texttt{assigns}} clause of
  \texttt{push} are established
\item the invariant \textcolor{blue}{\texttt{q\_invariant}} is preserved by
  \texttt{push}
\end{itemize}
\vfill

Proofs of these obligations
\begin{itemize}
\item with Simplify (100\%) and CVC Lite (67\%)
\item with Coq (100\%), very easy (6 lines of tactics)
\end{itemize}
\vfill
\end{slide}

\begin{slide}
  \title{Example: in-place list reversal}

\begin{minipage}[b]{0.5\textwidth}
\begin{small}
\begin{alltt}
typedef struct struct_list \{
  int hd;
  struct struct_list *tl;
\} *list;

list reverse(list p) \{
  list r = NULL;
  while (p != NULL) \{
    list q = p ; 
    p = p->tl; 
    q->tl = r; 
    r = q;
  \}
  return r;
\}
\end{alltt}
\end{small}
\end{minipage}
\hfill
\unitlength=1mm
\psset{unit=\unitlength}
\newcommand{\cons}{
\pspolygon[fillstyle=solid,fillcolor=yellow](-4,-2)(-4,2)(0,2)(0,-2)
\pspolygon[fillstyle=solid,fillcolor=cyan](0,2)(0,-2)(4,-2)(4,2)}
\begin{picture}(50,60)(0,-6)
\put(11,58){\makebox(0,0)[c]{\texttt{p}}%
\psline[linearc=5]{->}(-2,0)(-2,-6)}
\multiput(10,50)(0,-12){4}{\cons
\psline[linearc=5]{->}(2,0)(1.5,-3)(-1.5,-7)(-2,-10)}
\put(10,2){\cons
\psline[linearc=5]{-*}(2,0)(2,-6)}
\put(25,30){\makebox(0,0)[c]{\texttt{reverse(p)}}}
\put(25,30){\psline{->}(-6,-3)(6,-3)}
\multiput(40,38)(0,-12){4}{\cons
\psline[linearc=5]{->}(2,0)(1.5,3)(-1.5,7)(-2,10)}
\put(40,50){\cons
\psline[linearc=5]{-*}(2,0)(2,6)}
\put(41,-6){\makebox(0,0)[c]{\texttt{r}}%
\psline[linearc=5]{->}(-2,0)(-2,6)}
\end{picture}
\end{slide}

\begin{slide}
  \title{Introduction of new logical types and functions}

\begin{itemize}
\item Assertions are first-order logic formulas with a C-like syntax 
\item New predicates and functions can be introduced
\end{itemize}
\begin{small}
\begin{alltt}
// logical finite list of pointers
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
//@ logic plist nil()  
//@ logic plist cons(list p, plist l) 
\end{alltt}\end{minipage}}

// concatenation and reversal
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
//@ logic plist app(plist l1, plist l2) 
//@ logic plist rev(plist pl) 
\end{alltt}\end{minipage}}
\end{alltt}
\end{small}
\begin{itemize}
\item Axioms may be given, e.g.
\end{itemize}
\begin{small}
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
//@ axiom app\_nil : \bs{}forall plist l; app(nil(),l) == l 
\end{alltt}\end{minipage}}
\end{small}

\vfill
\end{slide}

\begin{slide}
  \title{Specification of list reversal}

\begin{small}
\begin{alltt}
/* llist(p,l) specifies that l is the list of pointers 
   from p to NULL following tl fields */
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
//@ predicate llist(list p, plist l) reads p->tl 
\end{alltt}\end{minipage}}
\adviwait
// is_list(p) specifies that p is finite 
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
//@ predicate is_list(list p) \{ \bs{}exists plist l ; llist(p,l) \} 
\end{alltt}\end{minipage}}
\adviwait


\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
/*@ requires is_list(p)
  @ ensures \bs{}forall plist l; 
  @    \old(llist(p, l)) => llist(\result, rev(l))  */
\end{alltt}\end{minipage}}
list reverse(list p);
\end{alltt}
\end{small}
\vfill
\end{slide}

\begin{slide}
  \title{Annotating the code of list reversal}

\begin{minipage}[b]{0.65\textwidth}
\begin{small}
\begin{alltt}
list reverse(list p) \{
  list r = NULL;
\colorbox{cyan}{\begin{minipage}{0.98\textwidth}\color{blue}\begin{alltt}
/*@ invariant 
   \bs{}exists plist lp; \bs{}exists plist lr;
     llist(p, lp) && llist(r, lr) && 
     disjoint(lp, lr) && 
     \bs{}forall plist l; \old(llist(p, l)) => 
       app(rev(lp), lr) == rev(l)
  @ variant length(p) for length_order */
\end{alltt}\end{minipage}}
  while (p != NULL) \{
    list q = p; 
    p = p->tl; q->tl = r; r = q;
  \}
  return r;
\}
\end{alltt}
\end{small}
\end{minipage}
\hfill
\unitlength=1mm
\psset{unit=\unitlength}
\newcommand{\cons}{
\pspolygon[fillstyle=solid,fillcolor=yellow](-4,-2)(-4,2)(0,2)(0,-2)
\pspolygon[fillstyle=solid,fillcolor=cyan](0,2)(0,-2)(4,-2)(4,2)}
\begin{picture}(20,60)(0,-6)
\put(1,38){\makebox(0,0)[c]{r}%
\psline[linearc=5]{->}(2,0)(6,0)}
\put(1,26){\makebox(0,0)[c]{p}%
\psline[linearc=5]{->}(2,0)(6,0)}
\multiput(10,50)(0,-12){5}{\cons}
\put(11,38){\psline[linearc=5]{->}(2,0)(1.5,3)(-1.5,7)(-2,10)}
\put(11,26){\psline[linearc=5]{->}(2,0)(1.5,-3)(-1.5,-7)(-2,-10)}
\put(11,14){\psline[linearc=5]{->}(2,0)(1.5,-3)(-1.5,-7)(-2,-10)}
\put(10,2){\cons
\psline[linearc=5]{-*}(2,0)(2,-6)}
\put(11,50){\psline[linearc=5]{-*}(2,0)(2,6)}
\end{picture}
\end{slide}

\begin{slide}
  \title{Certification of list reversal}
  
\begin{itemize}
\item 7 verification conditions
\item With Simplify: 71\%
\item With Coq: 100\%, with 661 lines of tactics
\end{itemize}
\vfill
\end{slide}

\begin{slide}
  \title{Example: Schorr-Waite algorithm}
  
\begin{itemize}
\item Graph marking algorithm
\item Considered as a benchmark for the verification of pointer programs
  (Bornat, 1999, Jape system) (Nipkow-Mehta, 2003, Isabelle/HOL)
\item 12 verification conditions
\item With Simplify: 33\%
\item With Coq: 100\%, with 2362 lines of tactics
%\item Note: termination remains to be proved\ldots
\end{itemize}
\vfill
\end{slide}

\begin{slide}
~\vfill
\begin{center}
  \textcolor{royalblue}{\hrulefill}\\[1em]

  \textcolor{royalblue}{\Large\bfseries Underlying Technique}

  \textcolor{royalblue}{\hrulefill}
\end{center}
\vfill\vfill
\end{slide}


\begin{slide}
  \title{Intermediate language: \Why{}}

\begin{center}
  \unitlength=4mm
  \psset{unit=\unitlength,colsep=1,shortput=nab,%
    arrows=->,labelsep=3pt,nodesep=3pt,%
    arrowlength=1,arrowinset=0.2,arm=8mm,linearc=3mm}
  \begin{picture}(20,15)(0,-5)
   \rput(10,10){\rnode{c}{\psframebox[linestyle=none,fillstyle=solid,fillcolor=lightgrey]{Annotated C program}}}
   \rput(10,7){\rnode{caduceus}{\psframebox[fillstyle=solid,fillcolor=lightred]{~~{\large \Caduceus}~~}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{c}{caduceus} 
   \rput(10,4){\rnode{whycode}{\psframebox[linestyle=none,fillstyle=solid,fillcolor=lightgrey]{\Why{} program}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{caduceus}{whycode} 
   \rput(10,1){\rnode{why}{\psframebox[fillstyle=solid,fillcolor=lightgreen]{~~{\large \Why}~~}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{whycode}{why} 
   \rput(10,-2){\rnode{vcg}{\psframebox[linestyle=none,fillstyle=solid,fillcolor=lightgrey]{Verification Conditions}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{why}{vcg} 
   \rput(0,-2){\rnode{coq}{\psframebox[fillstyle=solid,fillcolor=cyan]{~~Coq~~}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{vcg}{coq}
   \rput(2,-4.5){\rnode{pvs}{\psframebox[fillstyle=solid,fillcolor=cyan]{~~PVS~~}}} 
   \ncangle[linecolor=red,linewidth=4pt,angleA=-90,angleB=0,offsetA=-3]{->}{vcg}{pvs}
   \rput(10,-6){\rnode{simplify}{\psframebox[fillstyle=solid,fillcolor=yellow]{~~Simplify~~}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{vcg}{simplify}
   \rput(18,-4.5){\rnode{cvc}{\psframebox[fillstyle=solid,fillcolor=yellow]{~~CVC Lite~~}}} 
   \ncangle[linecolor=red,linewidth=4pt,angleA=-90,angleB=180,offsetA=3]{->}{vcg}{cvc}
   \rput(20,-2){\rnode{harvey}{\psframebox[fillstyle=solid,fillcolor=yellow]{~~haRVey~~}}}
   \ncline[linecolor=red,linewidth=4pt]{->}{vcg}{harvey}
\end{picture}
\end{center}
\end{slide}


\begin{slide}
\title{The Why tool}

\begin{itemize}
\item 
 Language \emph{dedicated} to program certification
  \begin{itemize}
  \item purely functional types + \emph{references} on such types
  \item Hoare-like annotations
    (pre/post-conditions, loop invariants/variants)
  \item explicit side effects: read/assigned references,
    exceptions raised
  \item aliases are forbidden
  \end{itemize}

\item Annotations are written in first-order predicate logic
%Expression of verification conditions only requires a
%  \emph{minimal logic} ($\forall$ $\Rightarrow$ $\land$)

 Adaptation to a new prover only requires a new
 \emph{pretty-printer} 

\item Allows abstract data types and functions

%  Une partie de la difficulté est en fait cachée dans le
%  \emph{modèle}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\title{Modeling C memory heap}

\begin{itemize}
\item Burstall-Bornat model: memory partition according to structure
  fields

\item We extend this idea to handle C arrays and pointer arithmetic: a
  memory block is

\newcommand{\carre}[1]{\multicolumn{#1}{|c|}{}}
\begin{footnotesize}
\begin{center}
  \begin{tabular}{rlllllll}
    &\qquad\qquad\qquad\qquad&&&\texttt{p}&\qquad\qquad\qquad&\texttt{p}&\hspace*{-1em}\texttt{+i=shift(p,i)}
    \\
    &\multicolumn{3}{c}{\leftarrowfill \texttt{offset(p)}\rightarrowfill}&
      $\downarrow$&&$\downarrow$
    \\\cline{2-8}
    \texttt{base\_addr(p)}&\carre{3}&\carre{1}&\carre{1}&\carre{1}&\carre{1}
    \\\cline{2-8}\\[-0.5em]
    &\multicolumn{7}{c}{\leftarrowfill \texttt{block\_length(alloc,p)}\rightarrowfill}
  \end{tabular}
\end{center}
\end{footnotesize}

\item Each structure field is a map from addresses to memory blocks

\end{itemize}
\vfill
\end{slide}


\begin{slide}
\title{Burstall-Bornat model: example of character queue}

\newcommand{\case}[1]{\multicolumn{1}{|c|}{#1}}
\newcommand{\ucase}{\multicolumn{1}{|c|}{~~}}
\newcommand{\nocase}{\multicolumn{1}{|c}{~~}}
\newcommand{\quatrecase}{\ucase&\ucase&\ucase&\ucase}
\newcommand{\cinqcase}{\ucase&\ucase&\ucase&\ucase&\ucase}
%\begin{center}
\begin{tabular}{cccccccccccccccccccc}

\emph{adresses} & \multicolumn{6}{c}{\emph{structure fields}} &
\multicolumn{6}{c}{\emph{arrays of} \texttt{int}} &
\\  
& \multicolumn{3}{c}{\texttt{last}} &  
\multicolumn{3}{c}{\texttt{contents}} & \qquad & 
\multicolumn{10}{c}{\texttt{intP}} \\
\cline{3-3} \cline{6-6}
q  && \case{\hbox to 0pt{4}\advirecord{q}{\colorbox{yellow}{5}}} &&& \case{\rnode{p}{}} &&& \nocase && 
\\
\cline{3-3}\cline{6-6}
  && \case{} &&& \case{} &&& \nocase && 
\\
\cline{3-3}\cline{6-6}\cline{9-18}
\rnode{pp}{}  && \nocase &&& \nocase &&& \quatrecase & \case{\advirecord{qq}{\hspace*{-0.3em}\colorbox{yellow}{c}\hspace*{-0.3em}}}& \cinqcase 
\\
\cline{9-18}
\ncangles[linearc=0.2,armA=0.7,angleB=-90,angleA=180,linecolor=darkgreen]{<-}{pp}{p}
\end{tabular}
%\end{center}

\vfill%\adviwait
\textcolor{blue}{\texttt{q.contents[q.last++] = c}}

\adviwait
\verb|q.last <- 4 + 1|
\adviwait
\adviplay{q}

\adviwait
\verb|*(q.contents+4) <- c|
\adviwait
\adviplay{qq}


%\begin{center}
% \begin{tabular}{cccccccccccccccccccc}
% \phantom{adresses} & \multicolumn{3}{c}{\texttt{last}} &  
% \multicolumn{3}{c}{\texttt{contents}} & \qquad & 
% \multicolumn{10}{c}{\texttt{intP}} \\
%  \cline{3-3} \cline{6-6}
% q  && \case{5} &&& \case{\rnode{p}{}} &&& \nocase && 
% \\
% \cline{3-3}\cline{6-6}
%   && \case{} &&& \case{} &&& \nocase && 
% \\
% \cline{3-3}\cline{6-6}\cline{9-18}
% \rnode{pp}{}  && \nocase &&& \nocase &&& \quatrecase & \case{c} & \cinqcase 
% \\
% \cline{9-18}
% \ncangles[linearc=0.2,armA=0.7,angleB=-90,angleA=180,linecolor=darkgreen]{<-}{pp}{p}
% \end{tabular}
%\end{center}

\end{slide}



\begin{slide}
\title{General structure of C memory heap}

\newcommand{\ucase}{\multicolumn{1}{|c|}{}}
\newcommand{\nocase}{\multicolumn{1}{|c}{}&&&&}
\newcommand{\unecase}{\ucase&&&&}
\newcommand{\troiscase}{\ucase&\ucase&\ucase&&}
\newcommand{\cinqcase}{\ucase&\ucase&\ucase&\ucase&\ucase}
\begin{footnotesize}
\begin{center}\hspace*{-10mm}
\begin{tabular}{c|c|ccccccccccccccccccccccccccccccccccccc}
\multicolumn{3}{r}{} \\
\multicolumn{2}{r}{\texttt{alloc}} & \quad &
\multicolumn{5}{c}{$f_1$} & $\cdots$ & 
\multicolumn{5}{c}{$f_k$} & \quad & 
\multicolumn{5}{c}{\texttt{intP}} & \quad&
\multicolumn{5}{c}{\texttt{intPP}} & \dots
\\
\multicolumn{2}{r}{} & &  \\
\cline{2-2}%\cline{4-4}\cline{6-6}\cline{8-8}\cline{10-10}
$a_1$  & n.a. & & \nocase & & \nocase & & \nocase & & \nocase &
\\
\cline{2-2}\cline{4-8}\cline{10-14}\cline{16-20}\cline{22-26}
$a_2$  & $5$ & & \cinqcase & & \cinqcase & & \cinqcase & & \cinqcase &
\\
\cline{2-2}\cline{4-8}\cline{10-14}\cline{16-20}\cline{22-26}
$a_3$  & $1$ & & \unecase & & \unecase & & \unecase & & \unecase &
\\
\cline{2-2}\cline{4-4}\cline{10-10}\cline{16-16}\cline{22-22}
$a_4$  & n.a. & & \nocase & & \nocase & & \nocase & & \nocase &
\\
\cline{2-2}\cline{4-6}\cline{10-12}\cline{16-18}\cline{22-24}
$a_5$  & $3$ & & \troiscase & & \troiscase & & \troiscase & & \troiscase &
\\
\cline{2-2}\cline{4-6}\cline{10-12}\cline{16-18}\cline{22-24}
$\vdots$  & $\vdots$    & & 
\multicolumn{1}{|c}{$\vdots$} &&&&&&
\multicolumn{1}{|c}{$\vdots$} &&&&&&
\multicolumn{1}{|c}{$\vdots$} &&&&&& 
\multicolumn{1}{|c}{$\vdots$} &&&& 
\end{tabular}
\end{center}
\end{footnotesize}
\vfill
\end{slide}


\begin{slide}
\title{Translation of C statements into Why}
The C statement 
\begin{alltt}
  q.contents[q.last++] = c
\end{alltt}
becomes in Why:
\begin{alltt}
assert valid(alloc,q);       \textcolor{blue}{// proof obligation}
let tmp1 = acc(last,q) in    \textcolor{blue}{// tmp1 <- q.last}
upd(last,q,tmp1+1);          \textcolor{blue}{// q.last <- tmp1+1}
let tmp2 = shift(acc(contents,q),tmp1) in 
                             \textcolor{blue}{// tmp2 <- q.contents + tmp1}
assert valid(alloc,tmp2);    \textcolor{blue}{// proof obligation}
upd(intP,tmp2,c)             \textcolor{blue}{// *tmp2 <- c}
\end{alltt}
\vfill
\end{slide}


\begin{slide}
\title{Axiomatization}

\begin{itemize}
\item The abstract Why functions \textcolor{blue}{\texttt{acc}},
  \textcolor{blue}{\texttt{upd}}, \textcolor{blue}{\texttt{shift}},
  etc. are specified by axioms: the \emph{background theory}. 

\item Excerpt from this theory:
\begin{alltt}
  acc(upd(t,i,v),i) = v
  i <> j -> acc(upd(t,i,v),j) = acc(t,j)
  shift(p,0) = p
  shift(shift(p,i),j) = shift(p,i+j)
...
\end{alltt}
\item An important part of this theory is dedicated to
  \textcolor{blue}{assigns} clauses
\end{itemize}

\vfill
\end{slide}

\begin{slide}

\title{Conclusion}

\begin{itemize}
\item We are able to certify non trivial programs
\item We support a large subset of ANSI C
\item Prototype freely available \textcolor{orange}{\url{http://why.lri.fr/caduceus}}\\\relax
 (Demo on demand)
\end{itemize}

But scaling up issues show up on large programs:

\begin{itemize}
\item Generated proof obligations can get large
\item Clear need for assistance to write specifications
\item Need for more automation of proofs, cooperation of provers
\end{itemize}
\vfill
\end{slide}

\begin{slide}

\title{Limitations}

Current limitations of the tool
\begin{itemize}
\item Non-terminating recursive functions
\item Initialization of global variables not satisfying invariants
\item Arithmetic overflow
\item Use of \verb|&| operator on stack-allocated variables
\item Dynamic memory allocation
\item \verb|union|
\end{itemize}

Limitations of the model:
\begin{itemize}
\item pointer cast
\item non ANSI features (i.e. compiler dependent)
\end{itemize}

\label{lastpage}
\adviwait\adviwait
\end{slide}


\begin{slide}
\title{About soundness of the approach}
\begin{enumerate}
\item Why method
  \begin{itemize}
  \item Why's verification condition generator has been proved\\\relax
    [Filliâtre, 2003, J. of Functional Programming]

  \item A \emph{validation} is produced: a certificate, checkable by
    Coq
  \end{itemize}

\item Caduceus translation from C to Why
  \begin{itemize}
  \item Soundness of the translation not formally proved but
  \item The modeling is simple enough to be trusted\\ its
    limitations are clearly exposed
  \item Ultimately, consistency of axioms can be proved by a Coq realization
  \end{itemize}
\end{enumerate}
\vfill
\end{slide}



\end{document}

\begin{slide}

\title{Future work}

  \begin{itemize}
    \item Mise au point des spécifications
      \begin{itemize}
      \item remontée de contre-exemples jusqu'à l'utilisateur 
      \item dépliage boucles
      \item évaluation symbolique sur des valeurs de test
      \end{itemize}
\adviwait
\bigskip
    \item Plus d'automatisation des preuves Coq
\adviwait
\bigskip
    \item Support plus complet de Java : arithmétique machine, code
      d'initialisation, etc.      
\adviwait
\bigskip
    \item Architecture multi-langages : C, OCaml, \dots
    \end{itemize}
\adviwait
\vfill
\begin{center}
FIN
\end{center}
\adviwait\adviwait
\label{lastpage}
\end{slide}

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