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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | en_US |
| Published: |
2003
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/3674 |
| _version_ | 1826212480435617792 |
|---|---|
| author | Rinard, Martin C. |
| author_facet | Rinard, Martin C. |
| author_sort | Rinard, Martin C. |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T15:22:16Z |
| format | Article |
| id | mit-1721.1/3674 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T15:22:16Z |
| publishDate | 2003 |
| record_format | dspace |
| spelling | mit-1721.1/36742019-04-12T08:08:46Z Credible Compilation * Rinard, Martin C. compiler credible compiler debugging proof checker optimization 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) 2003-11-16T18:04:36Z 2003-11-16T18:04:36Z 2003-01 Article http://hdl.handle.net/1721.1/3674 en_US Computer Science (CS); 177863 bytes application/pdf application/pdf |
| spellingShingle | compiler credible compiler debugging proof checker optimization Rinard, Martin C. Credible Compilation * |
| title | Credible Compilation * |
| title_full | Credible Compilation * |
| title_fullStr | Credible Compilation * |
| title_full_unstemmed | Credible Compilation * |
| title_short | Credible Compilation * |
| title_sort | credible compilation |
| topic | compiler credible compiler debugging proof checker optimization |
| url | http://hdl.handle.net/1721.1/3674 |
| work_keys_str_mv | AT rinardmartinc crediblecompilation |