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
 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 .
J.-C. Filliâtre and C. Marché designed a similar tool called
Caduceus  for dealing with C programs. This
tool was used by Th. Hubert and C. Marché  for
proving a subtle algorithm due to Schorr & Waite for graphs
traversal. J. Andronick  experimented on using
this tool for formal verification of security properties of smart card
embedded source code.
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
For his master work supervised by C.
Paulin, M. Sozeau  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
We developed several case studies in Coq
related to correctness of computer systems.
J.-F. Monin  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  developed libraries
for certifying termination proofs using dependent pairs criteria in
For his master work supervised by J-C. Filliâtre,
N. Ayache  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
Integrating automatic deduction into type theory is a long term
P. Corbineau [, ] made
a significant contribution extending results in first-order
intuitionistic logic with equality to the case of predicate defined by
constructors. S. Conchon [, ]
is studying decision procedures adapted to automatic resolution of
proof obligations generated by checking correctess of programs.
Mathematical proofs make an implicit use of
extensionality which identify two objects which are provably
equal. N. Oury  studied this rule and proposed a
translation of a derivation in an extensional sytem into an
intensional proof in a system like Coq.
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)
We also have a collaboration with César Muñoz at NIA, Hampton, USA
on proof of Java programs for avionics.
We participate to the new competitiveness cluster System@tic
(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.
D. Walukiewiecz and J. Chrzaszcz 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.
We have many exchanges (including a common seminar) with the LogiCal
project which is part of the INRIA site.
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”.
Sylvain Conchon and Sava Krstic.
Strategies for combining decision procedures.
Theoretical Computer Science, 2004.
Special Issue of TCS dedicated to a refereed selection of papers
presented at TACAS'03.
Claude Marché, Christine Paulin-Mohring, and Xavier Urbain.
The Krakatoa tool for certification of
Java/JavaCard programs annotated in JML.
Journal of Logic and Algebraic Programming, 58(1–2):89–106,
Sava Krstic and Sylvain Conchon.
Canonization for disjoint unions of theories.
Information and Computation, 2004.
Special Issue of Information and Computation dedicated to a refereed
selection of papers presented at CADE-19.
June Andronick, Boutheina Chetali, and Christine Paulin-Mohring.
Formal verification of security properties of smart card embedded
In John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, International Symposium of Formal Methods Europe (FM'05), volume 3582 of
Lecture Notes in Computer Science, Newcastle,UK, July 2005.
Evelyne Contejean and Pierre Corbineau.
Reflecting proofs in first-order logic with equality.
In 20th International Conference on Automated Deduction
(CADE-20), Lecture Notes in Computer Science, Tallinn, Estonia, July 2005.
Jean-Christophe Filliâtre and Claude Marché.
Multi-prover verification of C programs.
In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, Sixth
International Conference on Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science, pages 15–29, Seattle, WA, USA, November
Thierry Hubert and Claude Marché.
A case study of C source code verification: the Schorr-Waite
In 3rd IEEE International Conference on Software Engineering and
Formal Methods (SEFM'05), Koblenz, Germany, September 2005.
Bart Jacobs, Claude Marché, and Nicole Rauch.
Formal verification of a commercial smart card applet with multiple
In Algebraic Methodology and Software Technology, volume 3116
of Lecture Notes in Computer Science, Stirling, UK, July 2004.
Proof pearl: From concrete to functional unparsing.
In K. Slind, A. Bunker, and G. Gopalakrishnan, editors, International Conference on Theorem Proving in Higher Order Logics (TPHOLs
2004), volume 3223 of Lecture Notes in Computer Science, pages
217–224. Springer-Verlag, Park City, Utah, USA, September 2004.