VERIDIS

VeriDis is a joint research group of Inria Nancy, Max-Planck Institut für Informatik, CNRS and the Université de Lorraine. Its members in Nancy and Saarbrücken are experts in formal methods and verification. The objectives of the project are twofold: first, we exploit, further develop and integrate verification techniques (based on automated and interactive theorem proving, but also including model checking), where our main applicative focus is the area of concurrent and distributed algorithms and systems. Second, we contribute to sound methods that integrate formal verification techniques in the process of specifying, developing, and validating these 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 with a high degree of automation. 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. For example, the integration of relevant theories such as arithmetic in automated theorem proving has seen much progress in recent years. 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.