Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

A language-agnostic program verifier takes three inputs: a program, its formal specification, and the formal semantics of the programming language in which the program is written. It then uses a language-agnostic verification algorithm to prove the program correct with respect to its specification, using directly the formal language semantics. Such a complex verifier can easily have bugs. This paper proposes a method to certify the correctness of each successful verification run by generating a proof certificate for it. The proof certificate can be checked by a small proof checker. The preliminary experiments apply the method to generate proof certificates for the verification of an imperative language, a functional language, and an assembly language, showing that the proposed method is language-agnostic