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
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
