Wallenberg Academy Fellowsip 2014

TheProSE: Theorem Proving and Symbol Elimination
for Software Analysis and Verification

Principal Investigator: Laura Kovács
Funding Agency: Knut and Alice Wallenberg Foundation
Project Period: July 2015 - June 2020
Host Institution: Chalmers University of Technology


Project members

Events

Project overview: Computer systems are increasingly complex. Many companies are now routinely dealing with software comprising millions lines of code, written by people using different programming languages, tools and styles. This software is hard to understand and is integrated in an ever changing complex environment, using computers, networking, physical devices, security protocols and many other components. Software development practices are therefore costly and error prone.

Formal verification and program analysis provide methods for making reliable and robust systems, by proving that programs have no errors and thus are correct. The main idea behind these methods is to consider computer programs as mathematical objects and prove their properties in the same way as we prove theorems in mathematics. However, even if all scientists in the world start working exclusively on proving program properties, their work will take too long if not infinite time. Even then, only a tiny subset of implemented computer programs will be covered. The solution is to delegate the task of proving program properties to special kinds of computer programs proving program properties.

The objective of this project is to develop new rigorous methods helping to automatically analyze and verify computer systems.

Project tasks: Our project uses our recent symbol elimination method, as follows.

  • First, we will automatically derive program properties and hints that prevent programmers from introducing errors while making changes in programs.
  • Second, since program properties can be arbitrarily complex, we will design non-trivial algorithms for automated reasoning over program properties.
  • Third, we will implement world-leading tools supporting symbol elimination in software analysis and verification. Our workhorse will be the award-winning first-order theorem prover Vampire.

Our results will make a significant step towards reducing the number of errors in computer programs, and thereby reduce the costs of developing safe and reliable programs, bringing major benefits for individuals, society and industry.