Français Anglais
Accueil Annuaire Plan du site
Home > Groups > Research activities > Formalisation of (specification and programming) languages in proof assistants
Groups
Research activities: Formalisation of (specification and programming) languages in proof assistants



Groups
  Verification of Algorithms, Languages and Systems

Joint Inria project teams
  Toccata

Research highlights
  A Coq Formalization of the Relational Data Model
  Formal firewall conformance testing: an application of test and proof techniques

Contracts & grants
  HISSEO
  Typex
  Paral-ITP
  EURO-MILS
  VERASCO
  DIM COQUELICOT -Convention Proje
  HI-LITE

Software & patents
  HOL-TestGen
  HOL-OCL
  Le Système HOL-Z
  ALEA
  Isabelle/HOL
  The Coquelicot library
  CFML
  OntoEvent-B

Collaborations
  MBTSEC
  System X FSF

Members
  BENZAKEN Véronique
  CONTEJEAN Evelyne
  MARCHÉ Claude
  PAULIN-MOHRING Christine
  BOLDO Sylvie
  MANDEL Louis
  URBAIN Xavier
  WOLFF Burkhart
  LONGUET Delphine
  LELAY Catherine
  CHARGUERAUD Arthur
  DUMBRAVA Stéfania Gabriela
  NEMOUCHI Yakoub
  TUONG Frederic
  BALABONSKI Thibaut
  NGUYEN VAN Hai
  AIT-SADOUNE Idir
  VALIRON Benoît
  JOURDAN Jacques-Henri

Ph.D. dissertations & Faculty habilitations
  A Coq Formalization of Relational and Deductive Databases - and Mechanizations of Datalog
  Model-Based Testing of Operating System-level Security Mechanisms
  Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages
  De nouveaux réels pour Coq


Research activities