Download: PDF, slides (PDF), implementation.
“Building and using pluggable type-checkers” by Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Kıvanç Muşlu, and Todd Schiller. In ICSE 2011, Proceedings of the 33rd International Conference on Software Engineering, (Waikiki, Hawaii, USA), May 2011, pp. 681-690.
This paper describes practical experience building and using pluggable type-checkers. A pluggable type-checker refines (strengthens) the built-in type system of a programming language. This permits programmers to detect and prevent, at compile time, defects that would otherwise have been manifested as run-time errors. The prevented defects may be generally applicable to all programs, such as null pointer dereferences. Or, an application-specific pluggable type system may be designed for a single application.
We built a series of pluggable type checkers using the Checker Framework, and evaluated them on 2 million lines of code, finding hundreds of bugs in the process. We also observed 28 first-year computer science students use a checker to eliminate null pointer errors in their course projects.
Along with describing the checkers and characterizing the bugs we found, we report the insights we had throughout the process. Overall, we found that the type checkers were easy to write, easy for novices to productively use, and effective in finding real bugs and verifying program properties, even for widely tested and used open source projects.
Download: PDF, slides (PDF), implementation.
BibTeX entry:
@inproceedings{DietlDEMS2011,
author = {Werner Dietl and Stephanie Dietzel and Michael D. Ernst and
K{\i}van{\c{c}} Mu{\c{s}}lu and Todd Schiller},
title = {Building and using pluggable type-checkers},
booktitle = {ICSE 2011, Proceedings of the 33rd International
Conference on Software Engineering},
pages = {681--690},
address = {Waikiki, Hawaii, USA},
month = may,
year = {2011}
}