Files in this item



application/pdflin-chen-trinh-wang-rosu-2022-tr.pdf (546kB)
Main articlePDF


Title:Making Formal Verification Trustworthy via Proof Generation
Author(s):Lin, Zhengyao; Chen, Xiaohong; Trinh, Minh-Thai; Wang, John; Rosu, Grigore
Subject(s):Program verification
Proof generation
Abstract:Formal deductive verification aims at proving the correctness of programs via logical deduction. However, the fact that it is usually based on complex program logics makes it error-prone to implement. This paper addresses the important research question of how we can make a deductive verifier trustworthy through a practical approach. We propose a novel technique to generate machine-checkable proof objects to certify each verification task performed by the language-agnostic deductive verifier of K---a semantics-based language framework. These proof objects encode formal proofs in matching logic---the logical foundation of K. They have a small 240-line trust base and can be directly verified by third-party proof checkers. Our preliminary experiments show promising performance in generating correctness proofs for deductive verification in different programming languages.
Issue Date:2021-11-21
Genre:Technical Report
Date Available in IDEALS:2021-11-21

This item appears in the following Collection(s)

Item Statistics