Loading...
Please wait, while we are loading the content...
Similar Documents
Proof-carrying code with correct compilers
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Appel, Andrew W. |
| Copyright Year | 2009 |
| Description | In the late 1990s, proof-carrying code was able to produce machine-checkable safety proofs for machine-language programs even though (1) it was impractical to prove correctness properties of source programs and (2) it was impractical to prove correctness of compilers. But now it is practical to prove some correctness properties of source programs, and it is practical to prove correctness of optimizing compilers. We can produce more expressive proof-carrying code, that can guarantee correctness properties for machine code and not just safety. We will construct program logics for source languages, prove them sound w.r.t. the operational semantics of the input language for a proved-correct compiler, and then use these logics as a basis for proving the soundness of static analyses. |
| File Size | 34775 |
| Page Count | 1 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20150004716 |
| Archival Resource Key | ark:/13960/t9t200b2v |
| Language | English |
| Publisher Date | 2009-10-01 |
| Access Restriction | Open |
| Subject Keyword | Computer Programming And Software Computer Programming Languages Source Programs Semantics Proving Compilers Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
