Modular Reasoning about Software

For almost 40 years, computer science researchers have hoped to be able to mathematically verify properties of software. Despite a lot of research effort, most tools used in practice can still only verify simple properties. In particular, it has proved very difficult to develop tools to verify non-trivial properties of programs that use references to shared mutable data, ubiquitous in modern object-oriented languages. The consequence is that the developed tools will only work on small programs.

The goal of this project is to investigate and develop theories and methods for modular reasoning about software written in modern programming languages. The purpose is to lay the foundation for improvement of software tools, which are being and will be developed over the next five to ten years and which will be used to improve software practice. This is very important for society because software errors are extremely costly and can have fatal consequences.