Checker Framework

Preventing programming errors before they happen, via easy-to-use verification

Technologies
java
Topics
software engineering, verification, programmer productivity
Preventing programming errors before they happen, via easy-to-use verification

We are a group of developers who are passionate about code quality. We have built an innovative lightweight verification tool called the Checker Framework.

The Checker Framework helps you prevent bugs at development time, before they escape to production. It is based on the idea of pluggable type-checking. Pluggable type-checking replaces a programming language's built-in type system with a more powerful, expressive one.

Java's type system prevents some bugs, such as int count = "hello";. However, it does not prevent other bugs, such as null pointer dereferences, concurrency errors, disclosure of private information, incorrect internationalization, out-of-bounds indices, and so forth.

The Checker Framework enables you to create a more powerful type system and use it in place of Java's. The more powerful type system is not just a bug-finding tool: it is a verification tool that gives a guarantee that no errors (of certain types) exist in your program. Even though it is powerful, it is easy to use. It follows the standard typing rules that programmers already know, and it fits into their workflow. We have created around 20 new type systems, and other people have created many more.

The Checker Framework is popular: it is successfully used on hundreds of projects at Google, on Wall Street, and in other companies from big to small. It it attractive to programmers who care about their craft and the quality of their code. The Checker Framework is the motivation for Java's type annotations feature. Talks on it have received multiple awards at conferences such as JavaOne. With this widespread use, there is a need for people to help with the project: everything from bug fixes, to new features, to case studies, to IDE integration. We welcome your contribution!

Please see our ideas list for how to get started.

2017 Program

Successful Projects

Contributor
Felipe R. Monteiro
Mentor
Michael Ernst
Organization
Checker Framework
Whole-Program Inference
Checker Framework provides a collection of type systems to prevent bugs on Java programs at development time. Although a type system might be useful...
Contributor
Nikhil Deepak Shinde
Mentor
Michael Ernst, Mark Roberts
Organization
Checker Framework
Erroneous use of Java 8's Optional class
Traditionally, java programs use null to represent the absence of value. Java 8 introduced Optional class, a container that contains a reference to T...
Contributor
Vlastimil Dort
Mentor
Suzanne Millstein, Michael Ernst, Martin Kellogg
Organization
Checker Framework
Bounded-size strings
The goal of this project is to implement a checker for bounded-size strings in the Checker Framework, as described on the GSoC 2017 Ideas page. The...
Contributor
Bohdan Sharipov
Mentor
Suzanne Millstein, Michael Ernst
Organization
Checker Framework
Update to newer version of JavaParser
The JavaParser plays a significant role in the functioning of the StubParser project. The StubParser (sub-project of the Checker Framework) is the...
Contributor
Shinya Yoshida
Mentor
Suzanne Millstein, Werner Dietl
Organization
Checker Framework
Improving dataflow framework and analyzers
Checker Framework has a Dataflow Framework for Java Language. This is useful to infer more specific types in Checker Framework. This framework is not...