Keywords:
  - Diagnosis
  - Program proof
  - Software testing
  - Model-checking
  - Floating-point arithmetic

Groups
  Algorithms and Complexity
  Toccata
  Formal Testing and System Exploration

Joint Inria project teams


Research highlights
  Uniform trace sampling in very large models
  HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler
  One step forward: Linking wireless self-organizing network validation techniques with formal testing approaches
  On Theorem Prover-based Testing

Contracts & grants
  CAT
  CIFRE Dassault Aviation
  Software Factory
  VERAP
  GECCOO
  HOL-testGen XT

Software & patents
  sALLUSTe
  RUKIA
  CFML

Collaborations


Members
  MAGNIEZ Frédéric
  VIEILLERIBIERE Adrien
  GOURAUD Sandrine
  MESSIKA Stéphane
  FAYOLLE Julien
  STOULS Nicolas
  TRACOL Mathieu
  PEYRONNET Sylvain
  OUDINET Johan
  BARDOU Romain
  LESCUYER Stéphane
  BENTAKOUK Lina
  URRIBARRI Wendi
  LASSAIGNE Richard
  LALLALI Mounir

Ph.D. dissertations & Faculty habilitations
  Preuves mécanisées de propriétés de programmes
  Using Combinatorial Structures for Statistical Testing
  Approximate Verification - Quantum Computing
  Observing self-stabilization
  Self-Testing for Approximate and Qantum Computing
  Automatic Modular Sataic Safety Checking for C Programs

° 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
° 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