Computer Algebra and Theorem Proving for Verified Software

Formal verification aims at providing a methodology that produces more reliable and robust systems. As the complexity of software increases, there is a growing industrial interest in applying formal methods for ensuring reliability of long-lived, high-quality software systems for a variety of safety-critical applications, e. g. networking, security, complex systems, autonomous devices, traffic control, etc. The successful development and application of powerful automated reasoning tools such as model checkers, static program analyzers, computer algebra algorithms, decision procedures for common data structures, as well as theorem provers for first and higher order logic opened new perspectives and challenges for the automated verification of software systems. The objective of the project is to develop new methods of combining computer algebra and first-order theorem proving in static analysis of programs. This will enable verification of programs that are beyond the power of existing methods since advanced computer algebra techniques and their combination with first-order theorem proving are not used in state-of-the-arts verification tools. We are going to develop new theory and algorithms for the automated synthesis of auxiliary program assertions that can be used to prove automatically the validity of safety and liveness properties of software. A key impediment in verifying such properties is the overhead associated with providing and checking auxiliary program annotations. Typical auxiliary assertions are loop invariants and conditions on ranking functions. The complexity comes from the program size and structure, the programming language, the language in which the assertions are represented, the logic used for expressing generated verification theorems, and limitations of the modern theorem provers used for proving them. Verification is in general undecidable when unbounded data types, such as arrays, lists, pointers and uninterpreted functions, are used. Therefore, the project is focused on developing methods that efficiently handle complex programs, reason about unbounded data types, automatically create program annotations and use novel methods to prove program correctness based on such annotations. More precisely, we are going to (i) deploy symbolic computation techniques that, contrarily to existing methods, would automatically infer polynomial invariants and ranking functions; (ii) combine theorem proving with computer algebra which, unlike state-of-the-art tools, would yield the automatic derivation of quantified invariants with quantifier alternations; (iii) combine the generation of verification conditions with the automatic derivation of loop invariants and ranking functions; (iv) exploit and extend the power of current theorem provers to reason about also non-linear arithmetical properties of programs. For achieving these goals, the research will follow four main directions: (1) assertion synthesis, (2) automated program verification, (3) proving program properties, and (4) designing and evaluating software tools. Our research project targets in particular the class of imperative (sequential) loops, and aims at developing new theories, technologies, and tools for the automated verification of such programs.