Groups
  Verification of Algorithms, Languages and Systems

Joint Inria project teams
  Toccata

Research highlights
  Formal firewall conformance testing: an application of test and proof techniques

Contracts & grants
  HISSEO
  U3CAT
  Bware
  VERASCO
  HI-LITE
  CIFRE ADACORE

Software & patents
  Alt-Ergo
  Frama-C
  CFML
  Iris

Collaborations
  CEA-LIST
  AdaCore SAS

Members
  FILLIÂTRE Jean-Christophe
  MARCHÉ Claude
  PAULIN-MOHRING Christine
  BOLDO Sylvie
  PASKEVYCH Andriy
  MELQUIOND Guillaume
  TAFAT BOUZID Asma
  CHARGUERAUD Arthur
  CLOCHARD Martin
  GONDELMANS Levs
  BALABONSKI Thibaut
  MBIADA NDJANDA Jacques Charles
  JOURDAN Jacques-Henri
  GARCHERY Quentin

Ph.D. dissertations & Faculty habilitations
  FILLIATRE.02-12-2011
  Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels
  Preuves par raffinement de programmes avec pointeurs
  Un système de types pragmatique pour la vérification déductive des programmes

° 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
° 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
° Massively distributed algorithms for complex data