Groups
  Verification of Algorithms, Languages and Systems

Joint Inria project teams


Research highlights
  Testing for refinement in Circus
  Formal firewall conformance testing: an application of test and proof techniques
  Test selection for traces refinement, Ana Cavalcanti and Marie-Claude Gaudel

Contracts & grants
  pimi
  EURO-MILS
  DATE

Software & patents
  AuGuSTe
  HOL-TestGen

Collaborations
  Université de York
  MBTSEC
  International Joint Project MoBasT
  System X FSF
  LSV, ENS Cachan

Members
  GAUDEL Marie-Claude
  VOISIN Frédéric
  ZAIDI Fatiha
  WOLFF Burkhart
  POIZAT Pascal
  LONGUET Delphine
  NGUYEN Huu Nghia
  KHEFIFI Rania
  NEMOUCHI Yakoub
  AISSAT Romain
  TUONG Frédéric
  BALABONSKI Thibaut

Ph.D. dissertations & Faculty habilitations
  A symbolic approach for the verification and the testing of service choreographies
  Méthodes d'aide à la revue d'un processus de test de logiciel basé sur des modèles (Model Based Testing)
  Random based testing of C program
  Model-Based Testing of Operating System-level Security Mechanisms
  Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages

° 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
° Formalisation and Proof of Numerical Programs
° Formalisation of (Specification and Programming) Languages in Proof Assistants
° 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