Making Formal Verification Trustworthy via Proof Generation

Lin, Zhengyao; Chen, Xiaohong; Trinh, Minh-Thai; Wang, John; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/112785 Copy

Description

Title

Making Formal Verification Trustworthy via Proof Generation

Author(s)

• Lin, Zhengyao
• Chen, Xiaohong
• Trinh, Minh-Thai
• Wang, John
• Rosu, Grigore

Date of Publication

2021-11-21

Keyword(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.

Type of Resource

text

Language

en

Identifiers: URI or URL

http://hdl.handle.net/2142/112785

Owning Collections