\documentclass[a4paper,12pt]{article}

\usepackage[latin1]{inputenc}
\usepackage[french]{babel}
\usepackage{fullpage}
\usepackage{url}
\pagestyle{empty}
\begin{document}

\begin{center}
  Proposition de stage de Master 2ème année \\
  \Large\bf Coopération d'outils de preuve interactifs et automatiques \\[2em]
\end{center}

\begin{flushleft}
\textbf{Laboratoire :} LRI -- CNRS 8623, Université Paris Sud, 91405
ORSAY Cedex \\
\textbf{Directeur de laboratoire :} M.~Beaudouin-Lafon
(\texttt{mbl@lri.fr}) \\
\textbf{Équipe :} Démonstration et Programmation
(\texttt{http://www.lri.fr/demons/}) \\
\textbf{Directeur de stage :} J.-C.~Filliâtre
(\texttt{filliatr@lri.fr}) \\
\end{flushleft}

\paragraph{Domaine.}
Ce stage s'inscrit dans le contexte de la vérification formelle de
programmes, c'est-à-dire la preuve assistée par ordinateur qu'un
programme vérifie une spécification donnée. Dans l'équipe
\emph{Démonstration et Programmation} du LRI, nous développons des
outils de vérification formelle de programmes Java et C.

\paragraph{Objectifs du stage.}
Ces logiciels de preuve de programme reposent eux-même sur des outils
d'assistance à la démonstration existants, certains étant interactifs
(Coq, PVS, HOL Light, Mizar) et d'autres purement automatiques
(Simplify, CVC Lite, haRVey). Pour l'instant ces outils ne collaborent
pas, ils ne sont que des alternatives. L'objectif de ce stage est de
permettre la collaboration entre ces divers outils de preuve.

Un premier objectif, modeste, consistera à interfacer l'assistant de
preuve interactif Coq~[1] avec les procédures de décision automatiques
Simplify~[2] et CVC Lite~[3]. Plus précisément, il s'agira de pouvoir
appeler ces procédures de décision à partir de Coq, en supposant leur
résultat correct. On s'attachera à mettre en place une technologie
aussi générique que possible, de manière à faciliter l'intégration
d'autres procédures de décision.

Un second objectif, plus ambitieux, consistera à interpréter les
traces de preuve fournies par CVC Lite pour les traduire en des
preuves Coq. Ce travail pourra s'appuyer sur une expérience similaire
menée dans l'assistant de preuve Isabelle~[4].

\paragraph{Pré-requis :} Programmation, Logique. Cours concerné : 2-7.

\bibliographystyle{plain}
\begin{thebibliography}{99}
\bibitem{1} L'assistant de preuve Coq. \url{http://coq.inria.fr/}
\bibitem{2} Simplify. \url{http://research.compaq.com/SRC/esc/Simplify.html}
\bibitem{3} CVC Lite \url{http://verify.stanford.edu/CVCL/}
\bibitem{4} Tom Harke. \emph{Toward a sound integration of Isabelle
    with combined decision
    procedures}. \url{http://www.cse.ogi.edu/~harke/RPE-paper.ps} 
\end{thebibliography}

\end{document}

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