The project aims at applying modern computational logic and algebraic techniques methods developed at the Research Institute for Symbolic Computation (RISC-Linz), Johannes Kepler University for concrete aspects of reliable software verification developed by the programming languages and compilers group from Eötvös Loránd University (ELTE) in Budapest.

Program (algorithm) verification has a long research tradition but, so far, had relatively little impact on practical software development in the industry. A notable exception is the use of verification techniques in the test of computer processors. However, the design and implementation of reliable software still is an important issue and any progress in this area will be of outmost importance for the future development of IT. The logically deep parts of the code are characterized by (nested) loops or recursions. These parts constitute the interesting part of the code. For these parts, formal program verification is an appropriate tool. Formal program verification will only be attractive for industrial applications if a major part of the actual verification task can be automated.

Formal verification stimulates advances in the study of new logic formalism as temporal logic. In this project we aim to emphasize the importance of combining effectively and efficiently different proving methods, computer algebra tools and automated reasoning engines developed by the RISC group for the purpose of automated theorem proving and deductive verification, and to apply them to a number of concrete examples given by the ELTE team (e.g. to support development of components of distributed safety critical applications).

The two research groups, the automated reasoning Theorema group from RISC and the programming languages and compilers group from ELTE, deal with similar or closely related problems in program verification. By using practical problems for testing the different methods developed by the two research groups, we will compare the effectiveness of the different approaches and we will identify the most appropriate ones, as well as the necessary improvements and combinations of methods which are more appropriate for solving concrete problems.

• Automated invariant generation by algebraic methods
• Automated Theorem Proving
• Verification of Mobile Code using Algebraic Methods