Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

Zhengyao Lin, Xiaohong Chen, Minh Thai Trinh, John Wang, Grigore Roşu

Research output: Contribution to journalArticlepeer-review


Previous work on rewriting and reachability logic establishes a vision for a language-agnostic program verifier, which takes three inputs: a program, its formal specification, and the formal semantics of the programming language in which the program is written. The verifier then uses a language-agnostic verification algorithm to prove the program correct with respect to the specification and 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. The proof certificate can be checked by a small proof checker. The preliminary experiments apply the method to generate proof certificates for program verification in an imperative language, a functional language, and an assembly language, showing that the proposed method is language-agnostic.

Original languageEnglish (US)
Article number77
JournalProceedings of the ACM on Programming Languages
Issue numberOOPSLA1
StatePublished - Apr 6 2023
Externally publishedYes


  • Matching Logic
  • Program Verification
  • Reachability Logic

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier'. Together they form a unique fingerprint.

Cite this