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

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

Ph.D. dissertations & Faculty habilitations
  FILLIATRE.02-12-2011
  Un langage unique pour à la fois développer des programmes et les prouver
  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