VerifiCard at INRIA

This is INRIA's homepage for the IST-funded project VerifiCard.


The INRIA VerifiCard research team spans over three INRIA research projects: LogiCal, Lande and Lemme. These projects work in the areas of interactive proof environments, object-oriented programming, security, model checkers, and program analysis, transformation, and verification. Within VerifiCard, we aim at formal verification of security properties for Java Card programs.

LogiCal (ex-Coq, INRIA Rocquencourt)

Lande (INRIA Rennes/IRISA)

Lemme (INRIA Sophia-Antipolis)

Research description

Role of INRIA in the project

Much of the research is centered around the proof assistant Coq, which is used as a common framework to combine each group's specific domain of competence. Coq has been successfully used to certify a large subset of the Java Card platform, including the Virtual Machine, the Runtime Environment, the Converter and the Byte Code Verifier, as well as to certify algorithmic techniques for program verification, namely model-checking and abstract interpretation. These formalisations form the basis of INRIA's contribution to the project.


For more information on the research done within VerifiCard at INRIA, see also the full list of publications.



Relevant links

Related projects at INRIA

For more information on VerifiCard, contact Gilles Barthe, Yves Bertot or Marieke Huisman.

Last modified: Fri Sep 19 17:12:13 MEST 2003