Formal verification of a compiler back-end generic checker program

DOI10.1007/3-540-46562-6_42MaRDI QIDQ2729960zbMATH OpenFDO

Authors Axel Dold, Vincent Vialard

Publication date 23 October 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46562-6_42

zbMATH Keywords

checker-based program verificationformal verificationgeneric specification

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computing methodologies and applications (68U99)

Recommendations

• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Construction of verified compiler front-ends with program-checking
• A Completely Verified Realistic Bootstrap Compiler
• scientific article; zbMATH DE number 2090288

Cited in

(9)

• A formally verified compiler back-end
• Construction of verified compiler front-ends with program-checking
• scientific article; zbMATH DE number 1374873 (Why is no real title available?)
• scientific article; zbMATH DE number 1543049 (Why is no real title available?)
• Correct programs without proof? On checker-based program verification
• A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Verification, Model Checking, and Abstract Interpretation
• Deductive binary code verification against source-code-level specifications

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Formal verification of a compiler back-end generic checker program

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2729960)