The Checker Framework

Are you tired of null pointer exceptions, unintended side effects, SQL injections, concurrency errors, mistaken equality tests, and other run-time errors that appear during testing or in the field?

The Checker Framework enhances Java’s type system to make it more powerful and useful. This lets software developers detect and prevent errors in their Java programs. The Checker Framework includes compiler plug-ins ("checkers") that find bugs or verify their absence. It also permits you to write your own compiler plug-ins.

Quick start: go directly to the Installation instructions and tutorial.

• Download: checker-framework.zip version 1.8.4, 1 Aug 2014 (includes source, platform-independent binary, tests, and documentation)
  Then, see the installation instructions and tutorial.
• Documentation:
  • Checker Framework Manual (PDF)
  • Checker Framework Manual (HTML)
  • Installation instructions
  • Tutorial
  • Javadoc API documentation
  • Changelog
• Source code repository (at Google Code): http://code.google.com/p/checker-framework/
  The Checker Framework Manual contains instructions on building from source.
• Inference tools automatically add annotations to your code, making it even easier to start using the checkers. You must download these tools separately.
  • To infer the @Nullable type qualifier, use Daikon
  • To infer the @NonNull type qualifier, use the Julia Analyzer, Nit, or JastAdd
  • To infer the @ReadOnly type qualifier, use Javarifier
• Optional related tools:
  • The Annotation File Utilities extract annotations from, and write annotations to, .java and .class files. It also provides a representation (called an “annotation file”) for annotations that is outside the source code or the .class file. The tools support both Java 5 annotations, and the type annotations defined in JSR 308.
    • annotation-tools.zip (01 Aug 2014)
    • source code repository
    • Documentation is included in the zip archive and in the repository.
  • The Type annotations compiler is fully backward-compatible. You can use it in place of javac without any change in behavior, except that you will be permitted to place annotations in more locations (or in comments) and to use type-checking plug-ins that take advantage of those new locations. Most users don't need it, since a compiled version (without source code) is already included in the Checker Framework distribution.
• Research papers:
  • About the Checker Framework itself:
    • Practical pluggable types for Java (a paper presented at the ISSTA 2008 conference) describes the design of the Checker Framework, and case studies that found bugs in real programs and yielded new insights about type systems.
    • Building and using pluggable type-checkers (a paper presented at the ICSE 2011 conference) evaluates the ease of pluggable type-checking with the Checker Framework. The type-checkers were easy to write, easy for novices to use, and effective in finding hundreds of errors in case studies of 2 million lines of code.
  • About type systems evaluated using the Checker Framework:
    • Javari: Adding reference immutability to Java (OOPSLA 2005) describes the Javari immutability checker. Also see Inference of reference immutability (ECOOP 2008) and Parameter reference immutability: Formal definition, inference tool, and comparison (J.ASE 2009).
    • Object and reference immutability using Java generics (ESEC/FSE 2007) and Ownership and immutability in generic Java (OOPSLA 2010) describes the IGJ and OIGJ immutability checkers.
    • Inference of field initialization (ICSE 2011) describes inference for the Rawness Initialization Checker.
    • Tunable static inference for Generic Universe Types (ECOOP 2011) describes inference for the Generic Universe Types type system.
    • A type system for regular expressions (FTfJP 2012) describes the Regex Checker.
    • Verification games: Making verification fun (FTfJP 2012) describes a general inference approach that, at the time, had only been implemented for the Nullness Checker.
    • Inference and checking of object ownership (ECOOP 2012) describes an ownership type system.
    • ReIm & ReImInfer: Checking and inference of reference immutability and method purity (OOPSLA 2012) describes the ReIm immutability type system.
    • JavaUI: Effects for controlling UI object access (ECOOP 2013) describes the GUI Effect Checker.
    • A type system for format strings (ISSTA 2014) describes the Format String Checker.

Support and community

If you have a question, then first see whether your question is answered in one of the manuals listed under Documentation below. If none of those documents answers your question, then use one of the mailing lists.

Documentation

• Checker Framework Manual (PDF, HTML)
• Installation instructions
• Tutorial
• FAQ (Frequently Asked Questions with answers)

Mailing lists

We welcome questions, suggestions, patches, reports about case studies, and other contributions. Please let us know how we can improve the Checker Framework!

• checker-framework-discuss: for general discussion about the Checker Framework for building pluggable type systems (view archives, view old archives)
• checker-framework-dev: to reach the developers who maintain and extend the Checker Framework (view archives, view old archives)

You can also use the mailing lists to give help. Here are just a few examples:

• Respond to questions.
• Report problems (in the implementation or the documentation) or request features.
• Write code, then share your bug fixes, new features, compiler plug-ins, or other improvements.
• Make suggestions regarding the specification.

Another way to help is to tell your friends and colleagues about the usefulness and practicality of type annotations, or to report your successes to the mailing lists.

Bug reports

To submit a bug report, use the mailing list or, preferably, the issue tracker:

• Checker Framework issue tracker (please read these instructions first)

Last updated: Aug 1, 2014