Towards a Trustworthy Semantics-Based Language Framework via Proof Generation
| Autor: | Xiaohong Chen, Zhengyao Lin, Grigore Rosu, Thai Trinh |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Correctness
Computer science Programming language Semantics (computer science) 020207 software engineering 02 engineering and technology computer.software_genre Object (computer science) Mathematical proof Task (project management) Formal grammar 020204 information systems Automated proof checking 0202 electrical engineering electronic engineering information engineering Key (cryptography) computer |
| Zdroj: | Computer Aided Verification ISBN: 9783030816872 CAV (2) |
| Popis: | We pursue the vision of anideal language framework, where programming language designers only need to define the formalsyntaxandsemanticsof 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 onproof 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 bothpracticalandtrustworthy. 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|