Formal methods & applications

Department 2 : Formal Methods

Team leader : Dominique Méry
Tel. : +33 3 83 59 20 19
Mail :





Mastering the quality of software-intensive systems is a subject of critical importance. Formal methods for specification and programming are based on sound mathematical and logical foundations and contribute to addressing this objective. The goals of our research group are focused on notations, formalisms, and mechanized tools for specifying, refining, and verifying algorithms and systems where parallelism, distributed and cloud computing, telecommunications, and security-critical applications are predominant.

Research themes

  • Design and specification methods  for distributed systems
  • Tools for the analysis and verification of systems
  • Automated and interactive deduction, interpreted theories

Software tools

Active cooperations

  • Common Inria project VeriDis with the Automated Reasoning Group at Max-Planck Institut for Informatics in Saarbrücken
  • NUI Maynooth (Rosemary Monahan et Adam Winstanley)
  • TU Vienna (Igor Konnov and Josef Widder)
  • Microsoft Research (Leslie Lamport)
  • ClearSy and Systerel, Aix-en-Provence


Modeling, specification, refinement, abstraction, automated deduction, SMT solving, proof assistant, verification platform