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
  Pactole

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 Frédéric
  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

° Algorithm control and hyper-parameter tuning
° Algorithms for networked systems
° Automated Proof, SMT and Applications
° Automated Reasoning
° Combinatorics
° Compilation and code optimization
° Data-Centric Languages and Systems
° Deductive Verification of Programs
° Digital Fabrication
° Distributed algorithms
° Distributed Design
° Engineering of interactive systems
° Fab lab
° Formal Model-Based Testing
° Formalisation and Proof of Numerical Programs
° Generative design methods
° Graph Theory
° Green networks
° Heterogeneous Wireless Networks
° High-performance computing
° Human-Computer Interaction
° Integration of Data and Knowledge
° Interaction and visualization paradigms
° Large scale modelling
° Massively distributed algorithms for complex data