Michael Ernst, Professor MIT

Michael Ernst is the specification lead for JSR 308, a Java extension that will be part of Java 7 and will make it easier for programmers to specify and use custom type systems.

His research aims to make software more reliable, more secure, and easier (and more fun!) to produce. His technical interests are primarily in software engineering, including static and dynamic program analysis, testing, security, type theory, programming language design, and verification. Some of his work has been commercialized into systems that help programmers do a better job; other projects are available free, for the same purpose.

Ernst is an Associate Professor in the MIT Department of Electrical Engineering & Computer Science, and is a member of MIT's Computer Science & Artificial Intelligence Lab (CSAIL). Ernst was previously a lecturer in the Rice University computer science department and a programmer, then researcher, at Microsoft. He holds a Ph.D. in Computer Science and Engineering from the University of Washington.

Presentation: "User-defined type systems for error detection and prevention"

Track: Five Things I Wish I Learned In College

Time: Friday 13:00 - 14:00

Location: Cornell

Abstract:

Types help to detect and prevent errors: types help programmers to organize and document data, and types allow tools to verify that a program does not violate the type system's constraints. However, there is often much information about a type that a programmer cannot express. User-defined type qualifiers can enrich the built-in type system, permitting more expressive compile-time checking and guaranteeing the absence of certain errors. Examples of type qualifiers are NonNull, ReadOnly, Interned, and Tainted.

We have created a framework for Java that a type system designer to define new type qualifiers, and to create compiler plug-ins that check their semantics and issue lint-like warnings. A programmer can then use these type qualifiers throughout a program to obtain additional guarantees about the program. Developers can create and use the type qualifiers that are most appropriate for their software. Our toolset is fully backward-compatible with Java 5 annotations (and even with pre-annotations Java 4). Type annotations are scheduled for full support in Java 7, as part of JSR 308.

In the talk, I will present case studies of 4 checkers for type qualifiers. Each one found errors in real software, and is freely available for download. I will also discuss how you can create your own type qualifiers and checkers.

Password protected Download slides