Tools and Methods for Scalable Software Verifications

The need for correct and reliable software pervades all branches of society, such as telecommunications, manufacturing, trade, healthcare, finance, defense, and research. While software correctness has many facets (usability, security, and so on), this project focuses on functional correctness of sequential programs.

The last 50 years have shown how difficult it is to construct software that works correctly. In the last 40 years researchers have endeavored to develop program logics for formal specification of software's intended behavior and to prove that it satisfies the specification.

So-called shared mutable data have proven to be especially problematic, yet are ubiquitous in widely use programming languages such as Java and C#. It is hard to express properties of such software and it is hard to conduct proofs about it.

In recent years progress has been made on two fronts: the development of program logics, notably separation logic, and the development of proof assistants. Separation logic allows one to focus a proof on only the relevant substructures of shared mutable data, but so far only smallish "toy" programs have been specified and proven using separation logic.

The goals of this project are therefore:
- To apply the above-mentioned theoretical advances to practice
- To develop prototype software tools for formal specification with separation logic
- To apply the prototypes in a realistic case study
- To give methodological advice on how to structure software so as to facilitate formal specification and proof about it, and give advice on how to conduct such proofs.