A formal basis for a program compilation proof tool

DOI10.1007/3-540-45614-7_28MaRDI QIDQ4808847zbMATH OpenFDO

Authors Luke Wildman

Publication date 12 August 2004

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2391/23910491.htm

Mathematics Subject Classification ID

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

Recommendations

• A formally verified compiler back-end
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Compilation as refinement
• Procedure compilation in the refinement calculus
• Verified Compilation and the B Method: A Proposal and a First Appraisal

Cited in

(7)

• Procedure compilation in the refinement calculus
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• scientific article; zbMATH DE number 3874584 (Why is no real title available?)
• Programming language elements for correctness proofs
• Compilation as refinement
• Towards Formal Proof Script Refactoring
• An algebraic approach to the design of compilers for object-oriented languages

This page was built for publication: A formal basis for a program compilation proof tool

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