Making Formal Verification Trustworthy via Proof Generation
Author(s)
Lin, Zhengyao
Chen, Xiaohong
Trinh, Minh-Thai
Wang, John
Rosu, Grigore
Issue Date
2021-11-21
Keyword(s)
Program verification
Proof generation
Date of Ingest
2021-11-21T00:09:30Z
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.
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.
