Files in this item

FilesDescriptionFormat

application/pdf

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

Description

Title:Trustworthy Program Verification via Proof Generation
Author(s):Zhengyao Lin; XIaohong Chen; Minh-Thai Trinh; John Wang; Grigore Rosu
Subject(s):Semantic framework
Proof generation
Proof checking
Program verification
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.
Issue Date:2021-08-22
Genre:Technical Report
Type:Text
Language:English
URI:http://hdl.handle.net/2142/110344
Date Available in IDEALS:2021-08-22


This item appears in the following Collection(s)

Item Statistics