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 |
| Early online date | Apr 6 2023 |
| DOIs | |
| State | Published - Apr 6 2023 |
Keywords
- Matching Logic
- Program Verification
- Reachability Logic
ASJC Scopus subject areas
- Software
- Safety, Risk, Reliability and Quality
Fingerprint
Dive into the research topics of 'Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier'. Together they form a unique fingerprint.Cite this
- APA
- Standard
- Harvard
- Vancouver
- Author
- BIBTEX
- RIS