Loading...
Please wait, while we are loading the content...
Similar Documents
Type-based verification of sssembly language for compiler debugging
| Content Provider | ACM Digital Library |
|---|---|
| Author | Necula, George C. Chlipala, Adam Schneck, Robert R. Chang, Bor-Yuh Evan |
| Abstract | It is a common belief that certifying compilation, which typically verifies the well-typedness of compiler output, can be an effective mechanism for compiler debugging, in addition to ensuring basic safety properties. Bytecode verification is a fairly simple example of this approach and derives its simplicity in part by compiling to carefully crafted high-level bytecodes. In this paper, we seek to push this method to native assembly code, while maintaining much of the simplicity of bytecode verification. Furthermore, we wish to provide experimental confirmation that such a tool can be accessible and effective for compiler debugging. To achieve these goals, we present a type-based data-flow analysis or abstract interpretation for assembly code compiled from a Java-like language, and evaluate its bug-finding efficacy on a large set of student compilers. |
| Starting Page | 91 |
| Ending Page | 102 |
| Page Count | 12 |
| File Format | |
| ISBN | 1581139993 |
| DOI | 10.1145/1040294.1040303 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2005-01-10 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Certified compilation Abstract interpretation Dependent types Bytecode verification Assembly code |
| Content Type | Text |
| Resource Type | Article |
