Photo Responsable

Team : SPI - Semantics, Proofs and Implementations

Axe : .

Team leader :

ThĂ©rèse Hardin

Short presentation

Dessin Bulles HAL Staff directory 1 software

The SPI team build formal tools for critical software. The language, called Focal, for specifications and programs, allows to mix declarations, definitions, properties and proofs in a compilation unit. Focal has strong object features (inheritance, late binding), high level generic parametrization, and an encapsulation mechanism. Proofs are currently done within Coq or by an automatic prover called Zenon which issues Coq proofs when it success. The compiler produces OCaml sources, Coq sources and automatic documentation (XML files). The distribution comes with an important library of algebraic structures. The development of Focal is done in collaboration with the team CPR of CEDRIC lab. CNAM and of researchers at INRIA.
The SPI team also works on the construction of a general model of security policies, which allow two compare specifications and implementations of access control policies. This model is to be described within Focal, which as already been successfully used to specify several security policies and their implementations (annex 17-Doc 2320 of Civil aviation - CPR team, SQL reference monitor).

formal specifications, proofs and automatic deduction, correctness of implementations, critical systems, deduction modulo

Selected publications