VERIDIS Research team

Modeling and Verification of Distributed Algorithms and Systems

Team presentation

The VeriDis project aims to exploit and further develop the advances and integration of interactive and automated theorem proving applied to the area of concurrent and distributed systems. The goal of our project is to assist algorithm and system designers to carry out formally proved developments, where proofs of relevant properties as well as bugs can be found fully automatically.

Automated as well as interactive deduction techniques have seen spectacular progress over the last decade, and these techniques have had substantial impact. In particular, they have been successfully applied to the verification and analysis of sequential programs, often in combination with static analysis and software model checking. In an ideal world, systems and their properties are specified in high-level, expressive languages, errors in specifications are discovered automatically, and finally, full verification is also performed completely automatically. Due to the inherent complexity of the problem this cannot be achieved in general.

However, we have observed important advances in automated and interactive theorem proving in recent years, to which we have also participated, in particular concerning the integration of relevant theories such as arithmetic in automated theorem proving. These advances suggest that a substantially higher degree of automation can be achieved in system verification over what is available in today's verification tools.

Powerful theorem provers are not a panacea for system verification: their use must be based on a sound methodology for modeling and verifying systems. We have substantial expertise in developing and applying formal methods for concurrent and distributed algorithms and systems. In particular, the concept of refinement in state-based modeling formalisms is central to our approach. It is important to ensure that these methods support effective reasoning about modern concepts in algorithm and system design.

Research themes

languages and formalisms for modeling distributed systems, automated theorem proving techniques and tools, decision procedures and SMT solving, interactive theorem proving, model checking, integrated verification platforms

International and industrial relations

Keywords: Formal methods Theorem proving Satisfiability modulo theories Model checking Distributed systems

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social