You are here


Leader: Thomas JENSEN

The goal of the Celtique project is to improve the security and reliability of software through software certificates that attest to the well-behavedness of a given software. We aim at providing certificates issued from semantic software analysis. The semantic analyses extract approximate but correct descriptions of software behaviour from which a proof of security can be constructed.

The analyses of relevance include numerical data flow analysis, control flow analysis for higher-order languages, alias and points-to analysis for heap structure manipulation and data race freedom of multi-threaded code.

Team created since: 1st july 2009
Associated establishments: Université de Rennes 1, Inria, INSA Rennes, ENS Rennes
Location: Rennes (35)