Next: Padova
Up: Cooperating sites
Previous: Novi Sad - Belgrade


Université Paris-Sud

The team at Université Paris Sud in Orsay, France has recognised skills in the development of interactive proof assistants (Coq) but also automatic proof tools based on rewriting (Cime). It has developed specialised tools (Why, Krakatoa) on top of Coq for verification of programs written in C or Java. It is also recognised for its contribution to dependent type theory, in particular modules, combination with rewriting, inductive types and program extraction.

The team will mainly contribute to the objectives of Correctness of Computer Systems and Proof Technology.

The senior members are

Our research on development of certified Java programs is funded by the IST VERIFICARD project and the national ACI Geccoo. The national project RNTL AVERROES (analysis and verification for the reliability of embedded systems) uses the Coq system for the modelling and verification of systems described by a general class of timed-automata.

Paris Sud homepage


Bengt Nordström 2005-09-22