Français Anglais
Accueil Annuaire Plan du site
Accueil > Equipes > Activités de recherche > Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
Equipes
Formalisation de langages (de spécification et de programmation) dans les assistants de preuve



Equipes
  Vérification d'Algorithmes, Langages et Systèmes

Equipes-projets Inria communes
  Toccata

Resultats majeurs
  ESOP 2014 : A Coq Formalization of the Relational Data Model
  Formal firewall conformance testing: an application of test and proof techniques

Contrats
  HISSEO
  Typex
  Paral-ITP
  EURO-MILS
  VERASCO
  DIM COQUELICOT
  HI-LITE

Logiciels et brevets
  HOL-TestGen
  HOL-OCL
  Le Système HOL-Z
  ALEA
  Isabelle/HOL
  The Coquelicot library
  CFML
  OntoEvent-B
  Pactole

Collaborations
  MBTSEC
  System X FSF

Membres
  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 Frédéric
  BALABONSKI Thibaut
  NGUYEN VAN Hai
  AIT-SADOUNE Idir
  VALIRON Benoît
  JOURDAN Jacques-Henri

Thèses et habilitations
  Formalisation en Coq de Bases de Données Relationnelles et Déductives - et Mécanisation de 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


Activités de recherche
° Algorithmes pour les grands volumes de données distribuées
° Algorithmique des systèmes en réseau
° Algorithmique distribuée
° Architectures parallèles
° biologie de synthese
° Biologie des systèmes
° Biologie structurale
° biologie synthetique
° Calcul à haute performance
° Calcul quantique
° Calibration d'algorithmes (sélection, ajustement d'hyper-paramètres)
° Codage réseau
° Collaboration médiatisée
° Combinatoire
° Compilation et optimisation des programmes
° Décision optimale en contexte incertain
° Définition de nouveaux critères
° Démonstration automatique, SMT et applications
° Formalisation et preuves de programmes numériques
° Gestion de données du Web
° Ingénierie des systèmes interactifs
° Intégration de données et de connaissances
° Interaction Homme-Machine
° Langages et systèmes centrés données
° Méthodes de conception générative