Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

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

doi:10.1145/3586029

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 journal › Article › peer-review

Abstract

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 language	English (US)
Article number	77
Journal	Proceedings of the ACM on Programming Languages
Volume	7
Issue number	OOPSLA1
DOIs	https://doi.org/10.1145/3586029
State	Published - Apr 6 2023
Externally published	Yes

Keywords

Matching Logic
Program Verification
Reachability Logic

ASJC Scopus subject areas

Software
Safety, Risk, Reliability and Quality

Online availability

10.1145/3586029

Library availability

Discover UIUC Full Text

Cite this

@article{308032e9956e48c488ef44b849823c37,

title = "Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier",

abstract = "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.",

keywords = "Matching Logic, Program Verification, Reachability Logic",

author = "Zhengyao Lin and Xiaohong Chen and Trinh, {Minh Thai} and John Wang and Grigore Ro{\c s}u",

note = "The work presented in this paper was supported in part by an IOHK grant and an Ethereum Foundation gift. This material is based upon work supported by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092.",

year = "2023",

month = apr,

day = "6",

doi = "10.1145/3586029",

language = "English (US)",

volume = "7",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "OOPSLA1",

}

TY - JOUR

T1 - Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

AU - Lin, Zhengyao

AU - Chen, Xiaohong

AU - Trinh, Minh Thai

AU - Wang, John

AU - Roşu, Grigore

N1 - The work presented in this paper was supported in part by an IOHK grant and an Ethereum Foundation gift. This material is based upon work supported by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092.

PY - 2023/4/6

Y1 - 2023/4/6

N2 - 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.

AB - 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.

KW - Matching Logic

KW - Program Verification

KW - Reachability Logic

UR - http://www.scopus.com/inward/record.url?scp=85153750798&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85153750798&partnerID=8YFLogxK

U2 - 10.1145/3586029

DO - 10.1145/3586029

M3 - Article

AN - SCOPUS:85153750798

SN - 2475-1421

VL - 7

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - OOPSLA1

M1 - 77

ER -

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

Abstract

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this