It is surprisingly difficult to create software that can be trusted to work. For most software, correctness is inferred by extensive and costly testing, but this can only prove the presence of errors, not their absence. For safety-critical software, this is unsatisfactory. The ideal is to specify desired behaviours using logics and mathematics, and formally prove that the software satisfies its specification.
The aim of this project is to develop the scientific foundations for writing specifications and proofs of software written in modern programming languages. The combination of features in these languages, such as shared mutable state, higher-order functions, object-oriented design, and advanced control flow (e.g. exception-handling), make programs written in these languages difficult to verify.
This project will work on two fronts simultaneously. The first is to provide an environment (Charge!) where researchers can prototype new programming languages and specification logics and prove that programs are correct with respect to their specifications inside the interactive proof asssistant Coq. The second is to provide an Eclipse perspective (Kopitiam) that extends on the current Java perspective of Eclipse and allows users to verify the correctness of Java programs in the same environment as in which they write their programs. The ultimate goal is to have a tool where users can write their programs, their specifications, their models, and prove that the programs satisfy their specifications to the letter - and at the same time have all proofs checked by a state of the art interactive proof assistant.
We are funded by a Sapere Aude grant from the Danish Ministry of Science, Innovation and Higher Education (grant number 0602-03007B).