\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{url}
\oddsidemargin 0cm
\topmargin -1cm
\headsep 5mm
\textwidth 17cm
\textheight 24cm

%\newcommand{\url}[2]{#2\footnote{#1}}
\title{University Paris Sud (Orsay) site \\ and Grenoble and France
  Telecom R\& D subsites}
\author{C. Paulin}
\date{1/09/2004-31/08/2005}
\newcommand{\coq}{\textsf{Coq}}
\begin{document}
\maketitle



\section{Major scientific results}
\subsection{Correctness of Computer Systems}
\paragraph{Proving C or Java programs}

Our main activity is related to program verification. We mainly focus
on the verification of behavioral specifications for programming
languages such as C, Java and ML.  We develop a tool ''Why'' which is
a verification conditions generator: from an annotated program written
in a small imperative language with Hoare logic-like specification, it
generates conditions expressing the correctness and termination of the
program. These verification conditions can be generated for several
existing provers, including interactive proof assistants (\coq{}, PVS,
HOL Light, Mizar) and automatic provers (Simplify, haRVey, CVC Lite).

On top of this tool, we built a system called Krakatoa
\cite{marche04jlap} which verifies Java source code annotated with the
Java Modeling Language (JML).  The main challenge was the design of a
suitable model for the Java memory heap in order to tackle programs
with possible aliases~\cite{marche05tphols}.

J.-C. Filli�tre and C. March� designed a similar tool called
Caduceus~\cite{filliatre04icfem} for dealing with C programs. This
tool was used by Th. Hubert and C. March�~\cite{hubert05sefm} for
proving a subtle algorithm due to Schorr \& Waite for graphs
traversal. J. Andronick~\cite{andronick05fm} experimented on using
this tool for formal verification of security properties of smart card
embedded source code.

\paragraph{Timed  automata} 
Orsay and France Telecom R\& D collaborated on the definition
of a model of timed automata in \coq{}. It is integrated
in the CALIFE platform, a general tool for specification and automatic
or interactive verification of protocols. We are currently studying
the quantitative analysis of behavior of protocols built on random
choices. 


\paragraph{Dependent types} For his master work supervised by C.
Paulin, M. Sozeau~\cite{sozeau05master} designed a language with a
subset type (in the spirit of the PVS language) which is convenient
for programming with (a restricted class of) dependent types. He
proposed a translation of a term in this language to a \coq{} term
containing existential variables corresponding to type-checking
conditions.

\paragraph{Case studies} We developed several case studies in \coq{}
related to correctness of computer systems. \\
J.-F. Monin~\cite{monin04tphols} from
Grenoble subsite proved that the functional sprintf fonction of Danvy
and the usual version of sprintf (with a dependent typing) are
intensionally equal.  Th. Hubert~\cite{hubert04dea} developed libraries
for certifying termination proofs using dependent pairs criteria in
\coq{}.

\subsection{Formal Mathematics and Mathematics Education}
J. Duprat together with L. Vuillon from the Chambery subsite is
working on formalizing discrete geometry by inductive objects.
\subsection{Proof Technology}
For his master work supervised by J-C. Filli�tre,
N. Ayache~\cite{ayache05master} designed an interactive tactic for
calling first-order automatic provers from the \coq{} proof assistant. The
main difficulty was to derive an apropriate first-order theory from an
higher-order environment. 

\subsection{Foundational Research}
\paragraph{Automatic deduction}
Integrating automatic deduction into type theory is a long term
research.
P.~Corbineau~\cite{corbineau05these,contejean05cade} made
a significant contribution extending results in first-order
intuitionistic logic with equality to the case of predicate defined by
constructors.  S. Conchon~\cite{conchon-krstic-04,krstic-conchon-04}
is studying decision procedures adapted to automatic resolution of
proof obligations generated by checking correctess of programs.

\paragraph{Extensionality} Mathematical proofs make an implicit use of
extensionality which identify two objects which are provably
equal. N. Oury~\cite{oury05tphols} studied this rule and proposed a
translation of a derivation in an extensional sytem into an
intensional proof in a system like \coq{}.



\section{Cooperation with industry}
We are collaborating with Dassault Aviation in the area of proofs of C
programs. We also have a collaboration with the Axalto company (a
smartcards manufacturer) on proofs of Java and C programs, Javacard
applets and operating systems. Th. Hubert (Dassault), J. Andronick and
N. Rousset (Axalto) are studying for their PhD part-time in the
industry and part-time in our laboratory.

There is a collaboration between Orsay, Grenoble and the industrial
subsite France T�l�com R\& D in the AVERROES national project
(analysis and verification for the reliability of embedded systems)
(\url{http://www-verimag.imag.fr/AVERROES}).

We also have a collaboration with C�sar Mu\~noz at NIA, Hampton, USA
on proof of Java programs for avionics. 

We participate to the new competitiveness cluster System@tic
(\url{http://www.systematic-paris-region.org}). In this
cluster, the main industrial and academic research centers in the
Ile-de-France Region are collaborating in the area of complex systems. 

\section{List of visitors from other sites}
D. Walukiewiecz and J. Chrz{\k a}szcz from Warsaw University
visited our site in June
2005. They gave a seminar on ``Consistency and Completeness of
Rewriting in the Calculus of Constructions''.
Patryk Czarnik a Phd student from Warsaw University visited the Orsay
group 4 days in april 2005 and gave a seminar on his experiment using
the Krakatoa tool for proving Java programs.

\paragraph{Sites interactions}
We have many exchanges (including a common seminar) with the LogiCal
project which is part of the INRIA site.

\paragraph{Visit to other sites}
Jean-Christophe Filli�tre visited Queen Mary site in april 2005 and
gave a seminar on ``Verifying C and Java programs''.

\subsection{URL}
\url{http://www.lri.fr/demons/introduction.en.html}
\section{List of publications}
\renewcommand{\refname}{Refereed journal papers}
\begin{thebibliography}{10}
\bibitem{conchon-krstic-04}
Sylvain Conchon and Sava Krsti{\'c}.
\newblock Strategies for combining decision procedures.
\newblock {\em Theoretical Computer Science}, 2004.
\newblock Special Issue of TCS dedicated to a refereed selection of papers
  presented at TACAS'03.


\bibitem{contejean05jar}
Evelyne Contejean, Claude March{\'e}, Ana~Paula Tom{\'a}s, and Xavier Urbain.
\newblock Mechanically proving termination using polynomial interpretations.
\newblock {\em Journal of Automated Reasoning}, 2005.


\bibitem{marche04jlap}
Claude March{\'e}, Christine Paulin-Mohring, and Xavier Urbain.
\newblock The \textsc{Krakatoa} tool for certification of
  \textsc{Java/JavaCard} programs annotated in \textsc{JML}.
\newblock {\em Journal of Logic and Algebraic Programming}, 58(1--2):89--106,
  2004.
\newblock \url{http://krakatoa.lri.fr}.

\bibitem{marche2004jsc}
Claude March\'e and Xavier Urbain.
\newblock Modular and incremental proofs of {AC}-termination.
\newblock {\em Journal of Symbolic Computation}, 38:873--897, 2004.

\bibitem{krstic-conchon-04}
Sava Krsti{\'c} and Sylvain Conchon.
\newblock Canonization for disjoint unions of theories.
\newblock {\em Information and Computation}, 2004.
\newblock Special Issue of Information and Computation dedicated to a refereed
  selection of papers presented at CADE-19.
\end{thebibliography}

\renewcommand{\refname}{Refereed conferences papers}
\begin{thebibliography}{10}
\bibitem{andronick05fm}
June Andronick, Boutheina Chetali, and Christine Paulin-Mohring.
\newblock Formal verification of security properties of smart card embedded
  source code.
\newblock In John Fitzgerald, Ian~J. Hayes, and Andrzej Tarlecki, editors, {\em
  International Symposium of Formal Methods Europe (FM'05)}, volume 3582 of
  {\em Lecture Notes in Computer Science}, Newcastle,UK, July 2005.
  Springer-Verlag.

\bibitem{contejean05cade}
Evelyne Contejean and Pierre Corbineau.
\newblock Reflecting proofs in first-order logic with equality.
\newblock In {\em 20th International Conference on Automated Deduction
  (CADE-20)}, Lecture Notes in Computer Science, Tallinn, Estonia, July 2005.
  Springer-Verlag.

\bibitem{filliatre04icfem}
Jean-Christophe Filli{\^a}tre and Claude March{\'e}.
\newblock Multi-prover verification of {C} programs.
\newblock In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, {\em Sixth
  International Conference on Formal Engineering Methods}, volume 3308 of {\em
  Lecture Notes in Computer Science}, pages 15--29, Seattle, WA, USA, November
  2004. Springer-Verlag.

\bibitem{hubert05sefm}
Thierry Hubert and Claude March\'e.
\newblock A case study of {C} source code verification: the {Schorr-Waite}
  algorithm.
\newblock In {\em 3rd IEEE International Conference on Software Engineering and
  Formal Methods (SEFM'05)}, Koblenz, Germany, September 2005.

\bibitem{jacobs04amast}
Bart Jacobs, Claude March{\'e}, and Nicole Rauch.
\newblock Formal verification of a commercial smart card applet with multiple
  tools.
\newblock In {\em Algebraic Methodology and Software Technology}, volume 3116
  of {\em Lecture Notes in Computer Science}, Stirling, UK, July 2004.
  Springer-Verlag.

\bibitem{marche05tphols}
Claude March� and Christine Paulin-Mohring.
\newblock Reasoning about {Java} programs with aliasing and frame conditions.
\newblock In Hurd and Melham \cite{tphols2005}.

\bibitem{monin04tphols}
Jean-Fran�ois Monin.
\newblock {Proof pearl: From concrete to functional unparsing}.
\newblock In K.~Slind, A.~Bunker, and G.~Gopalakrishnan, editors, {\em
  {International Conference on Theorem Proving in Higher Order Logics (TPHOLs
  2004)}}, volume 3223 of {\em Lecture Notes in Computer Science}, pages
  217--224. Springer-Verlag, Park City, Utah, USA, September 2004.

\bibitem{oury05tphols}
Nicolas Oury.
\newblock Extensionality in the {Calculus of Constructions}.
\newblock In Hurd and Melham \cite{tphols2005}.

\end{thebibliography}

\renewcommand{\refname}{PhD and Master thesis}
\begin{thebibliography}{10}
\bibitem{ayache05master}
Nicolas Ayache.
\newblock Coop�ration d'outils de preuve interactifs et automatiques.
\newblock Master's thesis, Universit{\'e} Paris 7, 2005.

\bibitem{corbineau05these}
Pierre Corbineau.
\newblock {\em D�monstration Automatique en Th�orie des Types}.
\newblock Th{\`e}se de doctorat, Universit{\'e} Paris-Sud, September 2005.


\bibitem{hubert04dea}
Thierry Hubert.
\newblock {Certification des preuves de terminaison en Coq}.
\newblock Rapport de {DEA}, Universit{\'e} Paris 7, September 2004.
\newblock In French.

\bibitem{sozeau05master}
Matthieu Sozeau.
\newblock {Coercion par pr{\'e}dicats en {Coq}}.
\newblock Master's thesis, Universit{\'e} Paris 7, 2005.

\end{thebibliography}

\renewcommand{\refname}{Manual}
\begin{thebibliography}{10}
\bibitem{CoqManualV8}
{The {Coq} Development Team}.
\newblock {\em {The Coq Proof Assistant Reference Manual -- Version V8.0}},
  April 2004.
\newblock \url{http://coq.inria.fr}.
\end{thebibliography}

\renewcommand{\refname}{Cross-references}
\begin{thebibliography}{10}
\bibitem{tphols2005}
J.~Hurd and T.~Melham, editors.
\newblock {\em Theorem Proving in Higher Order Logics: 18th International
  Conference, TPHOLs 2005}, Lecture Notes in Computer Science. Springer-Verlag,
  August 2005.
\end{thebibliography}


\end{document}

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