Zachary Ryan Anderson

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2007-1

January 4, 2007

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-1.pdf

Hybrid type checking is an approach to enforcing the well-typedness of programs that, where possible, uses static analysis to determine the types of expressions, and run-time checking when the precision of static analysis is insufficeint. This approach is useful for dependent type systems in which types are parameterized by run-time values of expressions. Deputy is a dependent type system for C that allows the user to describe bounded pointers, tagged unions, and null-terminated strings. Deputy runs in two phases. In the first phase, simple typing rules are applied. The typing rules prescribe the insertion of run-time checks for certain operations. In the second phase, static analysis is used to identify checks that must either always succeed or always fail. The former may safely be removed, and the latter signify typing errors. This report describes the second phase of Deputy.

Advisors: Eric Brewer

---

BibTeX citation:

@mastersthesis{Anderson:EECS-2007-1,
    Author= {Anderson, Zachary Ryan},
    Title= {Static Analysis of C for Hybrid Type Checking},
    School= {EECS Department, University of California, Berkeley},
    Year= {2007},
    Month= {Jan},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-1.html},
    Number= {UCB/EECS-2007-1},
    Abstract= {Hybrid type checking is an approach to enforcing the well-typedness of programs that, where possible, uses static analysis to determine the types of expressions, and run-time checking when the precision of static analysis is insufficeint. This approach is useful for dependent type systems in which types are parameterized by run-time values of expressions. Deputy is a dependent type system for C that allows the user to describe bounded pointers, tagged unions, and null-terminated strings. Deputy runs in two phases. In the first phase, simple typing rules are applied. The typing rules prescribe the insertion of run-time checks for certain operations. In the second phase, static analysis is used to identify checks that must either always succeed or always fail. The former may safely be removed, and the latter signify typing errors. This report describes the second phase of Deputy.},
}

EndNote citation:

%0 Thesis
%A Anderson, Zachary Ryan 
%T Static Analysis of C for Hybrid Type Checking
%I EECS Department, University of California, Berkeley
%D 2007
%8 January 4
%@ UCB/EECS-2007-1
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-1.html
%F Anderson:EECS-2007-1