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.