Français Anglais
Accueil Annuaire Plan du site
Home > Groups > Research activities > Deductive verification of programs
Groups
Research activities: Deductive verification of programs



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

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


Research activities
° 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
° Distributed algorithms
° Engineering of interactive systems
° 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
° Mediated collaboration
° Multi-hop wireless networks
° Network coding