Return to search

Credible Compilation *

This paper presents an approach to compiler correctness in which the compiler generates a proof that the transformed program correctly implements the input program. A simple proof checker can then verify that the program was compiled correctly. We call a compiler that produces such proofs a credible compiler, because it produces verifiable evidence that it is operating correctly. / Singapore-MIT Alliance (SMA)

Identiferoai:union.ndltd.org:MIT/oai:dspace.mit.edu:1721.1/3674
Date01 1900
CreatorsRinard, Martin C.
Source SetsM.I.T. Theses and Dissertation
Languageen_US
Detected LanguageEnglish
TypeArticle
Format177863 bytes, application/pdf
RelationComputer Science (CS);

Page generated in 0.0018 seconds