UW CSE professor Michael Ernst and former postdoc Werner Dietl (now a professor at the University of Waterloo) killed it at Oracle’s JavaOne conference in San Francisco this week, delivering three well-received talks that drew upon UW CSE research: “Preventing Errors Before They Happen,” “Collaborative Verification of the Information Flow for a High-Assurance App Store” (about the SPARTA project), and “Using Type Annotations to Improve Your Code.”
The common theme of the three talks was lightweight software verification. Ernst, Dietl and colleagues at UW CSE have created widely-used tools for verifying Java programs. In the course of their work, they observed that the usual approaches to verification are powerful but impractical. While the main success of formal verification is type systems, the built-in type system of a language like Java permits too many incorrect programs.
To address this, the UW team devised new ways to strengthen type systems, such as making them flow-sensitive, while retaining their speed and ease of use. They also created a tool called the Checker Framework that makes it easy to create a type system for all of Java.
The Checker Framework ships with dozens of powerful type systems that are very effective at finding bugs. More importantly, these type systems give a guarantee: if a type system does not issue any warnings, then the program contains no bugs (of a certain variety). The type systems are used at companies from Wall Street to Silicon Valley (Google runs them on hundreds of projects every day). Oracle was so impressed with the Checker Framework that they added syntactic support for it to the Java 8 language, enabling 9 million programmers to improve their code. The type systems are also backward compatible with previous versions of Java.
If you want to improve your Java code, download the Checker Framework here.