MOSEL-VERIDIS

Websites

Mosel

Veridis

Presentation

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

• veriT solver
• TLA+ Proof System
• Redlog – Computing with Logic
• EB2ALL code generator

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

Keywords

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