Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

Xiaohong Chen, Zhengyao Lin, Minh Thai Trinh, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We pursue the vision of an ideal language framework, where programming language designers only need to define the formal syntax and semantics of their languages, and all language tools are automatically generated by the framework. Due to the complexity of such a language framework, it is a big challenge to ensure its trustworthiness and to establish the correctness of the autogenerated language tools. In this paper, we propose an innovative approach based on proof generation. The key idea is to generate proof objects as correctness certificates for each individual task that the language tools conduct, on a case-by-case basis, and use a trustworthy proof checker to check the proof objects. This way, we avoid formally verifying the entire framework, which is practically impossible, and thus can make the language framework both practical and trustworthy. As a first step, we formalize program execution as mathematical proofs and generate their complete proof objects. The experimental result shows that the performance of our proof object generation and proof checking is very promising.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
EditorsAlexandra Silva, K. Rustan Leino
PublisherSpringer
Pages477-499
Number of pages23
ISBN (Print)9783030816872
DOIs
StatePublished - 2021
Event33rd International Conference on Computer Aided Verification, CAV 2021 - Virtual, Online
Duration: Jul 20 2021Jul 23 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12760 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference33rd International Conference on Computer Aided Verification, CAV 2021
CityVirtual, Online
Period7/20/217/23/21

Keywords

  • Proof checking
  • Proof generation
  • Semantic framework

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Towards a Trustworthy Semantics-Based Language Framework via Proof Generation'. Together they form a unique fingerprint.

Cite this