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. Among others, several INRIA teams are working in this area. 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.