< Back to previous page

Project

Certified semi-automated modular formal program verification

Source code annotations-based semi-automated modular formal verification is a promising approach for verifying security, safety, and correctness properties of programs. It marries high assurance with relatively good usability by engineers, by offering a debugging-like user experience. However, in the current state of the art, the formal verification tools themselves have not been formally verified to be free of bugs that could cause them to report successful verification incorrectly. In this PhD project, we develop an approach for extending semi-automated formal verification tools so that they produce, upon successful verification, a machine-checkable proof object certifying that the input program does indeed satisfy the stated property. We will validate the approach by extending the VeriFast tool for verifying C programs so that it produces Coq proof scripts certifying correctness of the program with respect to a Coq-formalized semantics of C such as CompCert or CH2O/Formalin.

Date:23 Oct 2020 →  1 Sep 2023
Keywords:program verification, theorem proving, computer security, program logic
Disciplines:Computational logic and formal languages, Computer system security, Computers and logic systems
Project type:PhD project