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