Bor-Yuh Evan Chang

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2008-186

December 29, 2008

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-186.pdf

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.

Advisors: George Necula

---

BibTeX citation:

@mastersthesis{Chang:EECS-2008-186,
    Author= {Chang, Bor-Yuh Evan},
    Title= {Type-Based Verification of Assembly Language},
    School= {EECS Department, University of California, Berkeley},
    Year= {2008},
    Month= {Dec},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-186.html},
    Number= {UCB/EECS-2008-186},
    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.},
}

EndNote citation:

%0 Thesis
%A Chang, Bor-Yuh Evan 
%T Type-Based Verification of Assembly Language
%I EECS Department, University of California, Berkeley
%D 2008
%8 December 29
%@ UCB/EECS-2008-186
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-186.html
%F Chang:EECS-2008-186