Trustworthy Program Verification via Proof Generation

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

Permalink

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

Description

Title

Trustworthy Program Verification via Proof Generation

Author(s)

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

Issue Date

2021-08-22

Keyword(s)

• Semantic framework
• Proof generation
• Proof checking
• Program verification

Date of Ingest

2021-08-22T15:29:07Z

Abstract

In an ideal language framework, language designers only need to define the formal semantics of their languages. Deductive program verifiers and other language tools are automatically generated by the framework. In this paper, we propose a novel approach to establishing the correctness of these autogenerated verifiers via proof generation. Our approach is based on the K language framework and its logical foundation, matching logic. Given a formal language semantics in K, we translate it into a corresponding matching logic theory. Then, we encode formal verification tasks as reachability formulas in matching logic. The correctness of one verification task is then established, on a case-by-case basis, by automatically generating a rigorous, machine-checkable mathematical proof of the associated reachability formula. Experiments with our proof generation prototype on various verification tasks in different programming languages show promising performance and attest to the feasibility of the proposed approach.

Type of Resource

text

Genre of Resource

technical report

Language

en

Permalink

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

Owning Collections