Wallenberg Academy Fellowsip 2014
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.
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.