Practical pluggable types for Java

Download: PDF, PostScript, Talk slides (PDF), Demo slides (PDF), Papi thesis (PDF), Checker Framework implementation.

“Practical pluggable types for Java” by Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. In ISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis, (Seattle, WA, USA), July 22-24, 2008, pp. 201-212.
A tool demonstration appeared as “Compile-time type-checking for custom type qualifiers in Java” by Matthew M. Papi, Mahmood Ali, and Michael D. Ernst. In Companion to Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2008), (Nashville, TN, USA), October 21-23, 2008.
A tool demonstration appeared as “Building and using pluggable type systems with the Checker Framework” by Michael D. Ernst. In ECOOP 2008 — Object-Oriented Programming, 22nd European Conference, (Paphos, Cyprus), July 9-11, 2008. Tool demo.
An extended version containing expanded explanations and also some additional material appeared as “Practical Pluggable Types for Java” by Matthew M. Papi. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), May 2008.
A tool description appeared as “Compile-time type-checking for custom type qualifiers in Java” by Matthew M. Papi and Michael D. Ernst. In Companion to Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2007), (Montréal, Canada), October 23-25, 2007, pp. 809-810.
A previous version appeared as “Pluggable type-checking for custom type qualifiers in Java” by Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. MIT Computer Science and Artificial Intelligence Laboratory technical report MIT-CSAIL-TR-2007-047, (Cambridge, MA), September 17, 2007.

Abstract

This paper introduces the Checker Framework, which supports adding pluggable type systems to the Java language in a backward-compatible way. A type system designer defines type qualifiers and their semantics, and a compiler plug-in enforces the semantics. Programmers can write the type qualifiers in their programs and use the plug-in to detect or prevent errors. The Checker Framework is useful both to programmers who wish to write error-free code, and to type system designers who wish to evaluate and deploy their type systems.

The Checker Framework includes new Java syntax for expressing type qualifiers; declarative and procedural mechanisms for writing type-checking rules; and support for flow-sensitive local type qualifier inference and for polymorphism over types and qualifiers. The Checker Framework is well-integrated with the Java language and toolset.

We have evaluated the Checker Framework by writing 5 checkers and running them on over 600K lines of existing code. The checkers found real errors, then confirmed the absence of further errors in the fixed code. The case studies also shed light on the type systems themselves.

Download: PDF, PostScript, Talk slides (PDF), Demo slides (PDF), Papi thesis (PDF), Checker Framework implementation.

BibTeX entry:

@inproceedings{PapiACPE2008,
   author = {Matthew M. Papi and Mahmood Ali and Correa Jr., Telmo Luis
	and Jeff H. Perkins and Michael D. Ernst},
   title = {Practical pluggable types for {Java}},
   booktitle = {ISSTA 2008, Proceedings of the 2008 International
	Symposium on Software Testing and Analysis},
   pages = {201--212},
   address = {Seattle, WA, USA},
   month = {July~22--24,},
   year = {2008}
}

(This webpage was created with bibtex2web.)

Back to Program Analysis Group publications.