University of Illinois Urbana-Champaign

Making Formal Verification Trustworthy via Proof Generation

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

Content Files
lin-chen-trinh-wang-rosu-2022-tr.pdf

Permalink

https://hdl.handle.net/2142/112785

Description

Title
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.
Type of Resource
text
Genre of Resource
technical report
Language
en
Permalink
http://hdl.handle.net/2142/112785

Owning Collections

Research and Tech Reports - Computer Science PRIMARY