Start Date: 2006-10-01 End Date: 2009-02-01
The main objective of the project is to advance the state-of-the-art in proving and checking techniques for information systems, and to apply them to concrete industrial problems. In more detail, by using practical problems for testing the different methods for proving and model checking, we will compare the effectiveness of different techniques, and we will identify the most appropriate ones, as well as the necessary adaptations, improvements, and combinations of methods which are more appropriate for solving industrial problems. In particular, we will put a special emphasis on combining automated reasoning with model checking, especially infinite-state model checking. As we want to test these methods in the context of their usage, a central task of the project is the testing and improvement of the techniques for program verification and synthesis, as well as the corresponding methods for finitary problems: circuit synthesis and verification, and reactive algorithms.
An important task is the practical demonstration of the various methods in an industrial context. For this we will develop appropriate standards and tools for the integration of the methods into a coherent library, supported by an intelligent user interface in natural language. By direct interaction with applications, new and interesting theoretical and algorithmic developments will be initiated.