The Checker Framework Manual:
Custom pluggable types for Java

Chapter 41 Troubleshooting, getting help, and contributing

The manual might already answer your question, so first please look for your answer in the manual, including this chapter and the FAQ (Chapter 40). If you think you have found a bug in the Checker Framework, please report it (see Section 41.2). For discussions of broad interest, you can use the mailing list, checker-framework-discuss@googlegroups.com. For archives and to subscribe, see https://groups.google.com/forum/#!forum/checker-framework-discuss. If you want to help out, you can give feedback (including on the documentation), choose a bug and fix it (start with those labeled “good first issue”), or select a project from the ideas list at https://checkerframework.org/manual/new-contributor-projects.html.

41.1 Common problems and solutions

• To verify that you are using the compiler you think you are, you can add -version to the command line. For instance, instead of running javac -g MyFile.java, you can run javac -version -g MyFile.java. Then, javac will print out its version number in addition to doing its normal processing.

41.1.1 Unable to compile the Checker Framework

If you get the following error while compiling the Checker Framework itself:

checker-framework/stubparser/dist/stubparser.jar(org/checkerframework/stubparser/ast/CompilationUnit.class):
warning: [classfile] Signature attribute introduced in version 49.0 class files is ignored in version 46.0 class files

and you have used Eclipse to compile the Checker Framework, then probably you are using a very old version of Eclipse. (If you install Eclipse from the Ubuntu 16.04 repository, you get Eclipse version 3.8. Ubuntu 16.04 was released in April 2016, and Eclipse 3.8 was released in June 2012, with subsequent major releases in June 2013, June 2014, and June 2015.) Install the latest version of Eclipse and use it instead.

41.1.2 Unable to run the checker, or checker crashes

If you are unable to run the checker, or if the checker or the compiler terminates with an error, then the problem may be a problem with your environment. (If the checker or the compiler crashes, that is a bug in the Checker Framework; please report it. See Section 41.2.) This section describes some possible problems and solutions.

• An error that includes java.lang.NoSuchFieldError: RELEASE means that you are not using the correct compiler (you are not using a Java 9+ compiler).
• If you get the error
```
com.sun.tools.javac.code.Symbol$CompletionFailure: class file for com.sun.source.tree.Tree not found
```
then you are using the source installation and file tools.jar is not on your classpath. See the installation instructions (Section 1.3).
• If you get an error like one of the following,
```
...\build.xml:59: Error running ${env.CHECKERFRAMEWORK}\checker\bin\javac.bat compiler
```
```
.../bin/javac: Command not found
```
```
error: Annotation processor 'org.checkerframework.checker.signedness.SignednessChecker' not found
```
then the problem may be that you have not set the CHECKERFRAMEWORK environment variable, as described in Section 39.6. Or, maybe you made it a user variable instead of a system variable.
• If you get one of these errors:
```
The hierarchy of the type ClassName is inconsistent

The type com.sun.source.util.AbstractTypeProcessor cannot be resolved.
  It is indirectly referenced from required .class files
```
then you are likely not using the Checker Framework compiler. Use either $CHECKERFRAMEWORK/checker/bin/javac or one of the alternatives described in Section 39.6.
• If you get the error
```
    java.lang.ArrayStoreException: sun.reflect.annotation.TypeNotPresentExceptionProxy
```
then an annotation is not present at run time that was present at compile time. For example, maybe when you compiled the code, the @Nullable annotation was available, but it was not available at run time.
• The Checker Framework sometimes runs out of memory when processing very large Java files, or files with very large methods.

If you get an error such as
```
error: SourceChecker.typeProcess: unexpected Throwable (OutOfMemoryError) while processing ...
  ; message: GC overhead limit exceeded
```
(all on one line), then either give the JVM more memory when running the Checker Framework, or split your files and methods into smaller ones, or both.
• Versions of Error Prone before 2.4.0 are incompatible with the Checker Framework. (More precisely, each version of Error Prone before 2.4.0 is compatible with only one specific version of the Checker Framework.) Those versions of Error Prone use outdated versions of the Checker Framework’s dataflow analysis library, each of which is compatible with only one version of the Checker Framework.

If you wish to use both Error Prone and the Checker Framework, then use Error Prone version 2.4.0 or later. If you cannot upgrade to Error Prone 2.4.0 or later, there is a way to still use both tools. The Gradle plugin documentation shows how to do so if you use the Gradle build system.
• Versions 0.9.0 and 0.9.1 of NullAway are compatible only with Checker Framework version 3.6.0 through 3.8.0. Those versions of NullAway use version 3.6.0 of the Checker Framework’s dataflow analysis library without shading it. As of version 0.9.2, NullAway uses a shaded version of the library, so this conflict no longer exists. If you want to use a version of the Checker Framework newer than 3.8.0 with NullAway in the same build, then use NullAway 0.9.2 or later.

41.1.3 Unexpected warnings not related to type-checking

This section gives solutions for some warning messages that are not related to type errors in your code.

• If you get an error like the following
```
error: scoping construct for static nested type cannot be annotated
error: scoping construct cannot be annotated with type-use annotation
```
then you have probably written something like one of the following:

@Nullable java.util.List

The correct Java syntax to write an annotation on a fully-qualified type name is to put the annotation on the simple name part, as in java.util.@Nullable List. But, it’s usually better to add import java.util.List to your source file, so that you can just write @Nullable List.

@Nullable Map.Entry

You must write Outer.@Nullable StaticNestedClass rather than @Nullable Outer.StaticNestedClass. Since a static nested class does not depend on its outer class, the annotation on the outer class would have no effect and is forbidden.

Java 8 requires that a type qualifier be written directly on the type that it qualifies, rather than on a scoping mechanism that assists in resolving the name. Examples of scoping mechanisms are package names and outer classes of static nested classes.

The reason for the Java 8 syntax is to avoid syntactic irregularity. When writing a member nested class (also known as an inner class), it is possible to write annotations on both the outer and the inner class: @A1 Outer. @A2 Inner. Therefore, when writing a static nested class, the annotations should go on the same place: Outer. @A3 StaticNested (rather than @ConfusingAnnotation Outer. Nested where @ConfusingAnnotation applies to Outer if Nested is a member class and applies to Nested if Nested is a static class). It’s not legal to write an annotation on the outer class of a static nested class, because neither annotations nor instantiations of the outer class affect the static nested class.

Similar arguments apply when annotating pakkage.Outer.Nested.
• An “error: package ... does not exist” or “error: cannot find symbol” about classes in your own project or its dependencies means that you have left your own project or its dependencies off the classpath when you invoked the compiler.

41.1.4 Unexpected type-checking results

This section describes possible problems that can lead the type-checker to give unexpected results.

• If the Checker Framework is unable to verify a property that you know is true, then you should formulate a proof about why the property is true. Your proof depends on some set of facts about the program and its operation. State them completely; for example, don’t write “the field f cannot be null when execution reaches line 22”, but justify why the field cannot be null.

Once you have written down your proof, translate each fact into a Java annotation.

If you are unable to express some aspect of your proof as an annotation, then the type system is not capable of reproducing your proof. You might need to find a different proof, or extend the type system to be more expressive, or suppress the warning.

If you are able to express your entire proof as annotations, then look at the Checker Framework error messages.
- – Perhaps your proof was incomplete or incorrect. Your proof might depend on some fact you didn’t write down, such as “method m has no side effects”. In this case, you should revise your proof and add more annotations to your Java code.
- – Perhaps your proof is incorrect, and the errors indicate where.
- – Perhaps there is a bug in the type-checker. In this case, you should report it to the maintainers, giving your proof and explaining why the type-checker should be able to make the same inferences that you did.
Recall that the Checker Framework does modular verification, one procedure at a time; it observes the specifications, but not the implementations, of other methods.

Also see Section 2.4.5, which explains this same methodology in different words.
• If a checker seems to be ignoring the annotation on a method, then it is possible that the checker is reading the method’s signature from its .class file, but the .class file was not created by a Java 8 or later compiler. You can check whether the annotations actually appear in the .class file by using the javap tool.

If the annotations do not appear in the .class file, here are two ways to solve the problem:
- – Re-compile the method’s class with the Checker Framework compiler. This will ensure that the type annotations are written to the class file, even if no type-checking happens during that execution.
- – Pass the method’s file explicitly on the command line when type-checking, so that the compiler reads its source code instead of its .class file.
• If a checker issues a warning about a property that it accepted (or that was checked) on a previous line, then probably there was a side-effecting method call in between that could invalidate the property. For example, in this code:
```
if (currentOutgoing != null && !message.isCompleted()) {
    currentOutgoing.continueBuffering(message);
}
```
the Nullness Checker will issue a warning on the second line:
```
warning: [dereference.of.nullable] dereference of possibly-null reference currentOutgoing
    currentOutgoing.continueBuffering(message);
    ^
```
If currentOutgoing is a field rather than a local variable, and isCompleted() is not a pure method, then a null pointer dereference can occur at the given location, because isCompleted() might set the field currentOutgoing to null.

If you want to communicate that isCompleted() does not set the field currentOutgoing to null, you can use @Pure, @SideEffectFree, or @EnsuresNonNull on the declaration of isCompleted(); see Sections 33.7.5 and 3.2.2.
• If a checker issues a type-checking error for a call that the library’s documentation states is correct, then maybe that library method has not yet been annotated, so default annotations are being used.

To solve the problem, add the missing annotations to the library (see Chapter 36). The annotations might appear in stub files (.astub files distributed with the checker’s source code) or in annotated libraries (which appear in https://github.com/typetools/).
• If the compiler reports that it cannot find a method from the JDK or another external library, then maybe the stub file for that class is incomplete.

To solve the problem, add the missing annotations to the library, as described in the previous item.

The error might take one of these forms:
```
method sleep in class Thread cannot be applied to given types
cannot find symbol: constructor StringBuffer(StringBuffer)
```
• If you get an error related to a bounded type parameter and a literal such as null, the problem may be missing defaulting. Here is an example:
```
mypackage/MyClass.java:2044: warning: incompatible types in assignment.
      T retval = null;
                 ^
  found   : null
  required: T extends @MyQualifier Object
```
A value can be assigned to a variable of type T extends @MyQualifier Object only if that value is of the bottom type, since the bottom type is the only one that is a subtype of every subtype of T extends @MyQualifier Object. The value null satisfies this for the Java type system, and it must be made to satisfy it for the pluggable type system as well. The typical way to address this is to call addStandardLiteralQualifiers on the LiteralTreeAnnotator.
• An error such as
```
MyFile.java:123: error: incompatible types in argument.
                        myModel.addElement("Scanning directories...");
                                           ^
  found   : String
  required: ? extends Object
```
may stem from use of raw types. (“String” might be a different type and might have type annotations.) If your declaration was
```
    DefaultListModel myModel;
```
then it should be
```
    DefaultListModel<String> myModel;
```
Running the regular Java compiler with the -Xlint:unchecked command-line option will help you to find and fix problems such as raw types.
• The error
```
error: annotation type not applicable to this kind of declaration
    ... List<@NonNull String> ...
```
indicates that you are using a definition of @NonNull that is a declaration annotation, which cannot be used in that syntactic location. For example, many legacy annotations such as those listed in Figures 3.2 and 3.3 are declaration annotations. You can fix the problem by instead using a definition of @NonNull that is a type annotation, such as the Checker Framework’s annotations; often this only requires changing an import statement.
• If Eclipse gives the warning
```
The annotation @NonNull is disallowed for this location
```
then you have the wrong version of the org.eclipse.jdt.annotation classes. Eclipse includes two incompatible versions of these annotations. You want the one with a name like org.eclipse.jdt.annotation_2.0.0.....jar, which you can find in the plugins subdirectory under the Eclipse installation directory. Add this .jar file to your build path.

• When one formal parameter’s annotation references another formal parameter’s name, as in this constructor:

public String(char value[], @IndexFor("value") int offset, @IndexOrHigh("value") int count) { ... }

you will get an error such as

[expression.unparsable] Expression in dependent type annotation invalid:
Use "#1" rather than "value"

Section 33.8 explains that you need to use a different syntax to refer to a formal parameter:

public String(char value[], @IndexFor("#1") int offset, @IndexOrHigh("#1") int count) { ... }

• The Checker Framework can issue false positive warnings in dead code. An example is

    void m() {
      String t = "";
      t.toString();
      try {
      } catch (Throwable e) {
          t.toString(); // Nullness Checker issues spurious (dereference.of.nullable)
      }
    }

• If the Checker Framework issues an error or warning that you cannot reproduce using a smaller test case, then try running the Checker Framework with the -AatfDoNotCache command-line argument. If the Checker Framework behaves differently with and without that command-line argument, then there is a bug related to its internal caches. Please report that bug at https://github.com/typetools/checker-framework/issues.

41.1.5 Unexpected compilation output when running javac without a pluggable type-checker

A message of the form

    error: annotation values must be of the form 'name=value'
          @LTLengthOf("firstName", "lastName") int index;
                      ^

is caused by incorrect Java syntax. When you supply a set of multiple values as an annotation argument, you need to put curly braces around them:

         @LTLengthOf({"firstName", "lastName"}) int index;

41.2 How to report problems (bug reporting)

If you have a problem with any checker, or with the Checker Framework, please file a bug at https://github.com/typetools/checker-framework/issues. (First, check whether there is an existing bug report for that issue.) If the problem is with an incorrect or missing annotation on a library, including the JDK, see Section 41.2.1. You can also use the issue tracker to make suggestions and feature requests. We also welcome pull requests with annotated libraries, bug fixes, new features, new checkers, and other improvements.

Please ensure that your bug report is clear and that it is complete. Otherwise, we may be unable to understand it or to reproduce it, either of which would prevent us from helping you. Your bug report should include at least the following 4 parts: commands, inputs, output, and expectation.

Commands

Provide one or more commands that can be pasted into a command shell to reproduce the problem.

In the simplest case, you will provide one command of the form javac -processor ... MyFile.java. In more complex cases, it might be a set of commands to clone a repository, check out a branch, and run a build command. Include commands to install software and set environment variables if necessary.

If you encountered the problem in an IDE, reproduce it from the command line; if you cannot, report the bug to the IDE integration. If you encountered the problem when using a build system, it is most useful to the Checker Framework developers if you provide a single javac command rather than a build file.

It can be helpful to add
-version -Aversion -AprintGitProperties -verbose -AprintVerboseGenerics
to the javac options. This causes the compiler to output debugging information, including its version number.

Inputs

Include all files that are necessary to reproduce the problem. This includes every file that is used by any of the commands you reported, and possibly other files as well. This is not necessary if the commands you provided obtain the code that is type-checked.

If you cannot share your code, create a new, small test case. (A small test case is helpful even if your code is not secret!) If the Checker Framework crashed, the progress tracing options (Section 37.12.4) can be helpful in determining which file the Checker Framework was processing when it crashed.

Minimization: If your command invokes a build system such as Gradle or Maven, it can be helpful to the maintainers if you are able to reduce it to a single javac invocation on a single file. This also rules out the possibility that the problem is with the build system integration rather than the checker itself. If you use an invasive annotation processor such as Lombok, then try to reproduce the problem without it — this will indicate whether the problem is in the Checker Framework proper or in its interaction with Lombok.

Output

Indicate exactly what the result was by attaching a file or using cut-and-paste from your command shell. Don’t merely describe it in words, don’t use a screenshot, and don’t provide just part of the output.

Expectation

If the problem is not a crash, then indicate what you expected the result to be, since a bug is a difference between desired and actual outcomes. Also, please indicate why you expected that result — explaining your reasoning can reveal how your reasoning is different than the checker’s and which one is wrong. Remember that the checker reasons modularly and intraprocedurally: it examines one method at a time, using only the method signatures of other methods.

It can also be helpful to indicate what you have already done to try to understand the problem. Did you do any additional experiments? What parts of the manual did you read, and what else did you search for in the manual? Without this information, the maintainers may give you redundant suggestions or may waste time re-doing work you have already done.

When reporting bugs, please focus on realistic scenarios and well-written code. We are sure that you can make up artificial code that stymies the type-checker! That is not a good use of your time to report, nor of the maintainers’ time to evaluate and fix.

41.2.1 Problems with annotated libraries

If a checker reports a warning because a library contains incorrect annotations, then please open a pull request that adds the annotations. If the library’s maintainers have added annotations, make a pull request to them. If the Checker Framework maintainers have added annotations, you can find the annotated source in https://github.com/typetools/.

If a checker reports a warning because a library is not annotated, please do not open a GitHub issue. Instead, we appreciate pull requests to help us improve the annotations. Alternatively or in the interim, you can use stub files as described in Section 36.5.

For either approach, please see Chapter 36 for tips about writing library annotations.

Thanks for your contribution to the annotated libraries!

41.3 Building from source

The Checker Framework release (Section 1.3) contains everything that most users need, both to use the distributed checkers and to write your own checkers. This section describes how to compile its binaries from source. You will be using the latest development version of the Checker Framework, rather than an official release.

41.3.1 Install prerequisites

You need to install several packages in order to build the Checker Framework. Follow the instructions for your operating system. If your OS is not listed, adapt the instructions for an existing OS; for example, other Linux distributions will be similar to Ubuntu.

Put the setting of the JAVA_HOME environment variable in a startup file such as .bash_profile or .bashrc, if JAVA_HOME is not already set appropriately. It must be the location of your JDK installation (not the JRE installation). You may need to log out and log back in for the setting to take effect.

Ubuntu

Run the following commands, which should be the same as those in checker/bin-devel/Dockerfile-ubuntu-jdkXX-plus, where XX is a JDK version such as 17, 21, 25, etc.:

(If your build fails because it is missing a package, try the commands there and report a bug in this manual.)

sudo apt -qqy update
# Dependencies for building and running the Checker Framework.
sudo apt -qqy install \
  ant \
  cpp \
  git \
  jq \
  jtreg8 \
  libcurl3-gnutls \
  make \
  maven \
  python3-requests \
  python3-setuptools \
  unzip \
  wget
# Dependencies for developing the Checker Framework.
sudo apt -qqy install \
  autoconf \
  devscripts \
  dia \
  graphviz \
  imagemagick \
  junit \
  latexmk \
  librsvg2-bin \
  libasound2-dev libcups2-dev libfontconfig1-dev \
  libx11-dev libxext-dev libxrender-dev libxrandr-dev libxtst-dev libxt-dev \
  pdf2svg \
  poppler-utils \
  rsync \
  shellcheck \
  shfmt \
  texlive-extra-utils \
  texlive-font-utils \
  texlive-fonts-recommended \
  texlive-latex-base \
  texlive-latex-extra \
  texlive-latex-recommended

# Install uv (manages Python dependencies).
curl -LsSf https://astral.sh/uv/install.sh | sh
export PATH=$HOME/.local/bin:$PATH

# Install prek (pre-commit hook).
uv tool install prek

# Install the JDK.
sudo apt -qqy install \
  openjdk-25-jdk \
&& update-java-alternatives --set java-1.25.0-openjdk-amd64
export JAVA25_HOME=/usr/lib/jvm/java-25-openjdk-amd64

You may have to answer questions about which time zone your computer is in.

In a startup file, write:

    export JAVA_HOME=${JAVA_HOME:-$(dirname "$(dirname "$(readlink -f "$(which javac)")")")}

macOS

If you employ homebrew to install packages, run the following commands:

brew   update
brew   install git graphviz ant maven librsvg poppler unzip make
brew   install --cask temurin17
brew   install --cask mactex

Note: Running brew install --cask temurin17 is only necessary if you do not already have a JDK that is compatible with the Checker Framework installed.

If echo $JAVA_HOME outputs nothing (that is, if the JAVA_HOME environment variable is not set), then write the following in a startup file:

export JAVA_HOME=$(/usr/libexec/java_home -v XX)

export JAVA_HOME=/Library/Java/JavaVirtualMachines/adoptopenjdk-XX.jdk/Contents/Home/

In the command, XX is a JDK version such as 17, 21, 25, etc.

Windows

To build on Windows 10 or later, run bash to obtain a version of Ubuntu (provided by the Windows Subsystem for Linux) and follow the Ubuntu instructions.

41.3.2 Obtain the source

Obtain the latest source code from the version control repository:

git clone https://github.com/typetools/checker-framework.git checker-framework
export CHECKERFRAMEWORK=$(pwd)/checker-framework

You might want to add an export CHECKERFRAMEWORK=... line to your .bashrc file.

41.3.3 Build the Checker Framework

1. As with any Gradle project, run ./gradlew assemble to build the Checker Framework:
```
    cd $CHECKERFRAMEWORK
    ./gradlew assemble
```
Your antivirus program (e.g., Windows Security Virus & threat protection) might make the build run very slowly, or might make it seem to stall. Just give it time.

If compilation fails, but you have not made any changes, then perhaps one of the supporting repositories is in an inconsistent state; see Section 41.3.7.
2. Once it is built, you may wish to put the Checker Framework’s javac even earlier in your PATH:
```
export PATH=$CHECKERFRAMEWORK/checker/bin:${PATH}
```
The Checker Framework’s javac ensures that all required libraries are on your classpath and boot classpath, but is otherwise identical to the javac Java compiler.

Putting the Checker Framework’s javac earlier in your PATH will ensure that the Checker Framework’s version is used.
3. If you wish to use Maven or Gradle, publish the Checker Framework artifacts to a local Maven repository by running ./gradlew publishToMavenLocal:
```
    cd $CHECKERFRAMEWORK
    ./gradlew publishToMavenLocal
```
Then use the Maven or Gradle instructions, but modify the version number for the Checker Framework artifacts. Use the version number that is output when you run ./gradlew version.
4. Test that everything works:
- • Run ./gradlew allTests:
```
    cd $CHECKERFRAMEWORK
    ./gradlew allTests
```
- • Run the Nullness Checker examples (see Section 3.5).

41.3.4 Build the Checker Framework Manual (this document)

1. Install needed packages; see Section 41.3.1 for instructions.
2. Run make in the docs/manual directory to build both the PDF and HTML versions of the manual.

41.3.5 Code style, IDE configuration, pull requests, etc.

Please see the Checker Framework Developer Manual.

41.3.6 Enable continuous integration builds

We strongly recommend that you enable continuous integration (CI) builds on your fork of the projects, so that you learn quickly about errors. See the CI instructions in the Checker Framework Developer Manual.

Debugging continuous integration builds

If a continuous integration job is failing, you can reproduce the problem locally. The CI jobs all run within Docker containers. Install Docker on your local computer, then perform commands like the following to get a shell within Docker:

docker pull mdernst/cf-ubuntu-jdk21
docker run -it mdernst/cf-ubuntu-jdk21 /bin/bash

Then, you can run arbitrary commands, including those that appear in the CI configuration files. For example:

git clone --filter=blob:none -b docker-ubuntu-24-10 https://github.com/mernst/checker-framework.git
cd checker-framework
export CHECKERFRAMEWORK=$(pwd)
alias javacheck='$CHECKERFRAMEWORK/checker/bin/javac'
export NO_WRITE_VERIFICATION_METADATA=true
checker/bin-devel/test-cftests-junit.sh

41.3.7 Related repositories

Building the Checker Framework depends on other repositories, such as Annotated JDK. You need to have compatible versions of each.

After you git pull in one of the repositories, you should do so in the others as well. The script checker/bin-devel/clone-related.sh pulls all the related repositories, so to build the latest development version of the Checker Framework you can do

cd $CHECKERFRAMEWORK
git pull
checker/bin-devel/clone-related.sh

41.4 Contributing

We welcome contributions and pull requests. Section 41.3 tells you how to set up your development environment to compile the Checker Framework, and the Checker Framework Developer Manual gives more information.

One good way to contribute is to give feedback about your use of the tool. There is a list of potential projects for new contributors at https://checkerframework.org/manual/new-contributor-projects.html. Or, you can fix a bug that you have encountered during your use of the Checker Framework.

41.4.1 Contributing fixes (creating a pull request)

Please see the pull requests section of the Checker Framework Developer Manual. Thanks in advance for your contributions!

The easiest bugs to fix for a newcomer are labeled as “good first issue”.

Please do not spam the issue tracker with requests to assign an issue to you. If you want to contribute by fixing an issue, just open a pull request that fixes it. You can do that even if the issue is already assigned to someone.

Please do not spam the issue tracker asking how to get started fixing a bug. If you have concrete questions, please ask them and we will be happy to assist you. If you don’t know how to get started fixing a particular bug, then you should contribute to the project in other ways. Thanks!

41.5 Credits and changelog

Differences from previous versions of the checkers and framework can be found in the docs/CHANGELOG.md file. This file is included in the Checker Framework distribution and is also available on the web at https://checkerframework.org/CHANGELOG.md.

Developers who have contributed code to the Checker Framework include Abhijit Kulkarni, Abraham Lin, Adian Qian, Aditya Singh, Akash Srivastava, Alex Liu, Alvin Abdagic, Anant Jain, Anatoly Kupriyanov, Andy Turner, Ankit Yadav, Aosen Xiong, Arie van Deursen, Artem Pyanykh, Arthur Baars, Ashish Rana, Asumu Takikawa, Atul Dada, Ayush Agarwal, Baorui Zhou, Basil Peace, Benno Stein, Bohdan Sharipov, Brian Corcoran, Calvin Loncaric, Charles Chen, Charlie Garrett, Chris Povirk, Chris Toxiadis, Christopher Mackie, Colin S. Gordon, Craig Day, Damika Anupama, Dan Brotherston, Dan Brown, Daniel Gao, Daniel Zhu, David Lazar, David McArthur, Di Wang, Dilraj Singh, Dmitriy Shepelev, Eric Spishak, Ethan Koenig, Farzan Mirshekari, Felipe R. Monteiro, Florian Lanzinger, Gagan Dhakrey, Gautam Korlam, Google Inc. (via @wmdietlGC), Haaris Ahmed, Haifeng Shi, Hamed Taghani, Heath Borders, Ivory Wang, Jakub Vrána, James Yoo, Jason Waataja, Javier Thaine, Jeff Luo, Jenny Xiang, Jeroen Meijer, Jianchu Li, Jiangqi Zhang, Jiasen (Jason) Xu, Joe Schafer, John Krah, John Vandenberg, JohnnyJayJay, Jonathan Burke, Jonathan Nieder, Joshua Peterson, Jugal Mistry, Junhao Hu, Kanak Das, Kartikeya Goswami, Kenneth Knowles, Kivanc Muslu, Konstantin Weitz, Kurt Alfred Kluever, Lazaro Clapp, Leo Liu, Liam Miller-Cushon, Lian Sun, Luqman Aden, Mahmood Ali, Manu Sridharan, Mark Roberts, Marko Bekhta, Markus Frohme, Martin Kellogg, Matt Mullen, Maximilian Gama, Michael Bayne, Michael Coblenz, Michael Ernst, Michael Hixson, Michael Sloan, Michal Stehlik, Mier Ta, Mrigank Arora, Muyeed Ahmed, Narges Shadab, Neil Brown, Nhat Dinh, Nhat Nguyen, Nicholas Breen, Nikhil Shinde, Nima Karimipour, Nitin Kumar Das, Oleg Shchelykalnov, Olek Wojnar, Pascal Wittmann, Patrick Meiring, Paul Vines, Paulo Barros, Philip Lai, Piyush Jha, Pratik Bhusal, Prionti Nasir, Priti Chattopadhyay, Rashmi Mudduluru, Ravi Roshan, Renato Athaydes, René Just, René Kraneis, Rob Bygrave, Rui Fernandes, Ruturaj Mohanty, Ryan Oblak, Sadaf Tajik, Sagar Tewari, Sanjay Malakar, Sascha Kehrli, Sean C. Sullivan, Sean McLaughlin, Sebastian Schuberth, Shinya Yoshida, Shubham Kapoor, Shubham Raj, Sidney Monteiro, Simon Gerst, Stefan Heule, Steph Dietzel, Stephan Schroevers, Stuart Pernsteiner, Suzanne Millstein, Thomas Schweizer, Thomas Weißschuh, Tony Wang, Trask Stalnaker, Travis Haagen, Utsav Oza, Vatsal Sura, Vitalii Ananiev, Vivek Singh Solanki, Vladimir Sitnikov, Vlastimil Dort, Weitian Xing, Werner Dietl, Yuki Yang, Zhiping Cai.

In addition, too many users to list have provided valuable feedback, which has improved the toolset’s design and implementation. Thanks for your help!

41.6 License

Two different licenses apply to different parts of the Checker Framework.

• The Checker Framework itself is licensed under the GNU General Public License (GPL), version 2, with the classpath exception. This is the same license that OpenJDK is licensed under. Just as compiling your code with javac does not infect your code with the GPL, type-checking your code with the Checker Framework does not infect your code with the GPL. Running the Checker Framework during development has no effect on your intellectual property or licensing.

If you want to ship the Checker Framework as part of your product, then your product may need to be licensed under the GPL. Because of the classpath exception, you can include parts of the Checker Framework in your product, even if your product uses a different license. For example, Google’s Error Prone and Uber’s NullAway both use the Checker Framework internally, but neither one is licensed under the GPL.
• The more permissive MIT License applies to code that you might want to include in your own program, such as the annotations and run-time utility classes.

For details, see file LICENSE.txt.

41.7 Publications

Here are some papers that use the Checker Framework; for instance, they build a type-checker on top of the Checker Framework, or their methodology depends on using the Checker Framework. (The list does not include papers that merely cite the Checker Framework.) This list is incomplete; if you know of a paper that is missing, please let us know so that we can add it. Most educational use of the Checker Framework is never published, and most commercial use of the Checker Framework is never discussed publicly. Most of the papers are available for free online; do a web search on the title.

• Practical pluggable types for Java (ISSTA 2008) [PAC⁺08]
• Building and using pluggable type systems with the Checker Framework (ECOOP 2008) [Ern08a]
• Type-Based Object Immutability with Flexible Initialization (ECOOP 2009) [HP09]
• The nullness analyser of Julia (LPAR 2010) [Spo10]
• Static checking of safety critical Java annotations (JTRES 2010) [TPV10]
• Ownership and immutability in generic Java (OOPSLA 2010) [ZPL⁺10]
• Rethinking the economics of software engineering (FOSER 2010) [SE10]
• Applying uniqueness to the Java language (Master’s Thesis, 2010) [Har10]
• TIFI+: A Type Checker for Object Immutability with Flexible Initialization (Diploma thesis, 2010) [Noa10]
• Building and using pluggable type-checkers (ICSE 2011) [DDE⁺11]
• Inference of field initialization (ICSE 2011) [SE11]
• EnerJ: approximate data types for safe and general low-power computation (PLDI 2011) [SDF⁺11]
• Tunable static inference for generic universe types (ECOOP 2011) [DEM11]
• Separating ownership topology and encapsulation with generic universe types (TOPLAS 2011) [DDM11]
• The design, implementation and evaluation of a pluggable type checker for thread-locality in Java (Master’s Thesis, 2011) [She11]
• Towards Effective Inference and Checking of Ownership Types (IWACO 2011) [HM11]
• Static Dominance Inference (TOOLS 2011) [MV11]
• A Static Memory Safety Annotation System for Safety Critical Java (RTSS 2011) [TPNV11]
• Inference and checking of object ownership (ECOOP 2012) [HDME12]
• A type system for regular expressions (FTfJP 2012) [SDE12]
• Verification games: making verification fun (FTfJP 2012) [DDE⁺12]
• Reim & ReImInfer: checking and inference of reference immutability and method purity (OOPSLA 2012) [HMDE12]
• ReImInfer: method purity inference for Java (FSE 2012) [HM12]
• Inference and checking of context-sensitive pluggable types (FSE 2012) [MH12]
• Documenting Java database access with type annotations (WorldComp 2012) [Ber12]
• Immutability (book chapter, 2013) [PÖZE13]
• JavaUI: Effects for controlling UI object access (ECOOP 2013) [GDEG13]
• Reified type parameters using Java annotations (GPCE 2013) [GBS13]
• Evaluating the Accuracy of Annotations in the Loci 3.0 Pluggable Type Checker (Master’s Thesis, 2013) [Zaz13]
• Composing polymorphic information flow systems with reference immutability (FTfJP 2013) [MH13]
• Type-based taint analysis for Java web applications (FASE 2014) [HDM14]
• A type system for format strings (ISSTA 2014) [WKSE14]
• Collaborative verification of information flow for a high-assurance app store (CCS 2014) [EJM⁺14]
• Cascade: A universal type qualifier inference tool (ICSE 2015) [VPEJ15]
• An inference and checking framework for context-sensitive pluggable types (PhD thesis, 2014) [Hua14]
• CFL-reachability and context-sensitive integrity types (PPPJ 2014) [MHD14]
• Static analysis of implicit control flow: resolving Java reflection and Android intents (ASE 2015) [BJM⁺15]
• Scalable and Precise Taint Analysis for Android (ISSTA 2015) [HDMD15]
• A context-sensitive security type system for Java (Master’s thesis, 2015) [Kai15]
• Locking discipline inference and checking (ICSE 2016) [ELM⁺16]
• Semantics for locking specifications (NFM 2016) [EMMS16]
• JCrypt: Towards computation over encrypted data (PPPJ 2016) [DMD16a]
• Preventing signedness errors in numerical computations in Java (FSE 2016) [Mac16]
• Enforcing correct array indexes with a type system (FSE 2016) [San16]
• Gradual Pluggable Typing in Java (Master’s Thesis, 2016) [Bro16]
• Security analysis of the IRMA app using SPARTA and fuzzing (Bachelor Thesis, 2016) [Bri16]
• Static Analysis and Program Transformation for Secure Computation on the Cloud (ISSTA 2016 Doctoral Symposium) [DMD16b]
• Towards using concurrent Java API correctly (ICECCS 2016) [LBSD16]
• Reflection-aware static analysis of Android apps (ASE 2016) [LBOK16]
• A crowdsourcing game for formal software verification (Bachelor’s thesis) [Iri16]
• Exploring Language Support for Immutability (ICSE 2016) [CSA⁺16]
• Granullar: Gradual nullable types for Java (CC 2017) [BDL17]
• Type checking for reliable APIs (WAPI 2017) [KS17]
• Glacier: transitive class immutability for Java (ICSE 2017) [CNA⁺17]
• A General Pluggable Type Inference Framework and its use for Data-flow Analysis (Master’s Thesis, 2017) [Li17]
• Null safety benchmarks for object initialization (ISP RAS, 2017) [Kog17]
• Static analysis and program transformation for secure computation on the cloud (PhD Thesis, 2017) [Don17]
• Spartan Jester: end-to-end information flow control for hybrid Android applications (SPW 2017) [SCN17]
• Lightweight verification of array indexing (ISSTA 2018) [KDME18]
• Safe Stream-based Programming with Refinement Types (ASE 2018) [SCSC18]
• Don’t miss the end: Preventing unsafe end-of-file comparisons (NFM 2018) [CD18]
• Context sensitive typechecking and inference: ownership and immutability (Master’s Thesis, 2018) [Ta18]
• Usable and Sound Static Analysis through its Integration into Automated and Interactive Workflows (Master’s Thesis, 2018) [Val18]
• Pluggable properties for program understanding: Ontic type checking and inference (Master’s Thesis, 2018) [Che18]
• Definite reference mutability (ECOOP 2018) [Mil18]
• Googletest to CUTE converter (Technical report, 2018) [GV18]
• NullAway: Practical type-based null safety for Java (ESEC/FSE 2019) [BCS19]
• Compile-time detection of machine image sniping (ASE 2019) [Kel19]
• Type-Directed Bounding of Collections in Reactive Programs (VMCAI 2019) [LČCT19]
• Scala with Explicit Nulls (Master’s Thesis, 2019) [NR19]
• A machine-checked proof of security for AWS Key Management Service (CCS, 2019) [ABB⁺19]
• Synthesis of assurance cases for software certification (ICSE NIER 2020) [BKM20]
• Verifying object construction (ICSE 2020) [KRS⁺20]
• Precise inference of expressive units of measurement types (OOPSLA 2020) [XLD20]
• Rethinking safe consistency in distributed object-oriented programming (OOPSLA 2020) [KEW⁺20]
• Continuous compliance (ASE 2020) [KSTE20]
• Light-weight verification of cryptographic API usage (Master’s Thesis, 2020) [Xin20]
• Type checking and whole-program inference for value range analysis (Master’s Thesis, 2020) [Xia20]
• User-Centered Design of Principled Programming Languages (PhD thesis, 2020) [Cob20]
• Behavioural types for memory and method safety in a core object-oriented language (APLAS 2020) [BFG⁺20]
• Scala with Explicit Nulls (ECOOP 2020) [NZL⁺20]
• Property Types in Java: Combining Type Systems and Deductive Verification (Master’s Thesis, 2021) [Lan21]
• Interval Type Inference: Improvements and Evaluations (Master’s Thesis, 2021) [Wan21]
• Coping with the reality: adding crucial features to a typestate-oriented language (Master’s Thesis, 2021) [dLM21]
• Java Typestate Checker (Coordination 2021) [MGR21]
• Ensuring correct cryptographic algorithm and provider usage at compile time (FTfJP 2021) [XCD21]
• Scalability and Precision by Combining Expressive Type Systems and Deductive Verification (OOPSLA 2021) [LWUD21]
• Automatic Annotation of Confidential Data in Java Code (FPS 2021) [BBRS21]
• Accumulation Analysis (ECOOP 2022) [KSSE22]
• Lightweight Verification via Specialized Typecheckers (PhD thesis, 2022) [Kel22]

Bibliography

[ABB⁺19] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Gregoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, and Serdar Tasiran. A machine-checked proof of security for AWS Key Management Service. In CCS 2019: Proceedings of the 21st ACM Conference on Computer and Communications Security, page 63–78, London, UK, November 2019.
[AQKE09] Shay Artzi, Jaime Quinonez, Adam Kieżun, and Michael D. Ernst. Parameter reference immutability: Formal definition, inference tool, and comparison. Automated Software Engineering, 16(1):145–192, March 2009.
[Art01] Cyrille Artho. Finding faults in multi-threaded programs. Master’s thesis, Swiss Federal Institute of Technology, March 15, 2001.
[BBRS21] Iulia Bastys, Pauline Bolignano, Franco Raimondi, and Daniel Schoepe. Automatic annotation of confidential data in Java code. In FPS 2021: 14th International Symposium on Foundations & Practice of Security, Paris, France, December 2021.
[BCS19] Subarno Banerjee, Lazaro Clapp, and Manu Sridharan. NullAway: Practical type-based null safety for Java. In ESEC/FSE 2019: The ACM 27th joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 740–750, Tallinn, Estonia, August 2019.
[BDL17] Dan Brotherston, Werner Dietl, and Ondřej Lhoták. Granullar: Gradual nullable types for Java. In CC 2017: 26th International Conference on Compiler Construction, pages 87–97, Austin, TX, USA, February 2017.
[Ber12] Paul L. Bergstein. Documenting Java database access with type annotations. In WorldComp 2012: Proceedings of The 2012 World Congress in Computer Science, Computer Engineering, and Applied Computing, 2012.
[BFG⁺20] Mario Bravetti, Adrian Francalanza, Iaroslav Golovanov, Hans Hüttel, Mathias S. Jakobsen, Mikkel K. Kettunen, and António Ravara. Behavioural types for memory and method safety in a core object-oriented language. In APLAS 2020: 18th Asian Symposium on Programming Languages and Systems, page 105–124, Fukuoka, Japan, November 2020.
[BJM⁺15] Paulo Barros, René Just, Suzanne Millstein, Paul Vines, Werner Dietl, Marcelo d’Amorim, and Michael D. Ernst. Static analysis of implicit control flow: Resolving Java reflection and Android intents. In ASE 2015: Proceedings of the 30th Annual International Conference on Automated Software Engineering, pages 669–679, Lincoln, NE, USA, November 2015.
[BKM20] Hamid Bagheri, Eunsuk Kang, and Niloofar Mansoor. Synthesis of assurance cases for software certification. In ICSE NIER, Proceedings of the 42nd International Conference on Software Engineering, New Ideas and Emerging Results Track, pages 61–64, Seoul, Korea, May 2020.
[Bri16] Laurens Brinker. Security analysis of the IRMA app using SPARTA and fuzzing. Bachelor thesis, Radboud University, Nijmegen, Netherlands, 2016.
[Bro16] Daniel Brotherston. Gradual pluggable typing in Java. Master’s thesis, U. of Waterloo, Waterloo, Ontario, Canada, 2016.
[CD18] Charles Zhuo Chen and Werner Dietl. Don’t miss the end: Preventing unsafe end-of-file comparisons. In NFM 2018: 10th NASA Formal Methods Symposium, pages 87–94, Newport News, VA, USA, April 2018.
[Che18] Zhuo Chen. Pluggable properties for program understanding: Ontic type checking and inference. Master’s thesis, U. of Waterloo, Waterloo, Ontario, Canada, 2018.
[CNA⁺17] Michael Coblenz, Whitney Nelson, Jonathan Aldrich, Brad Myers, and Joshua Sunshine. Glacier: Transitive class immutability for Java. In ICSE 2017, Proceedings of the 39th International Conference on Software Engineering, pages 496–506, Buenos Aires, Argentina, May 2017.
[Cob20] Michael Coblenz. User-Centered Design of Principled Programming Languages. PhD thesis, Carnegie Mellon University, aug 2020. TR CMU-CS-20-127.
[Cop05] Tom Copeland. PMD Applied. Centennial Books, November 2005.
[Cro06] Jose Cronembold. JSR 198: A standard extension API for Integrated Development Environments. https://jcp.org/en/jsr/detail?id=198, May 8, 2006.
[CSA⁺16] Michael Coblenz, Joshua Sunshine, Jonathan Aldrich, Brad Myers, Sam Weber, and Forrest Shull. Exploring language support for immutability. In ICSE 2016, Proceedings of the 38th International Conference on Software Engineering, pages 736–747, Austin, TX, USA, May 2016.
[Dar06] Joe Darcy. JSR 269: Pluggable annotation processing API. https://jcp.org/en/jsr/detail?id=269, May 17, 2006. Public review version.
[DDE⁺11] Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Kıvanç Muşlu, and Todd Schiller. Building and using pluggable type-checkers. In ICSE 2011, Proceedings of the 33rd International Conference on Software Engineering, pages 681–690, Waikiki, Hawaii, USA, May 2011.
[DDE⁺12] Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Nathaniel Mote, Brian Walker, Seth Cooper, Timothy Pavlik, and Zoran Popović. Verification games: Making verification fun. In FTfJP: 14th Workshop on Formal Techniques for Java-like Programs, pages 42–49, Beijing, China, June 2012.
[DDM11] Werner Dietl, Sophia Drossopoulou, and Peter Müller. Separating ownership topology and encapsulation with Generic Universe Types. ACM Transactions on Programming Languages and Systems, 33(6):20:1–62, December 2011.
[DEM11] Werner Dietl, Michael D. Ernst, and Peter Müller. Tunable static inference for Generic Universe Types. In ECOOP 2011 — Object-Oriented Programming, 25th European Conference, pages 333–357, Lancaster, UK, July 2011.
[dLM21] João Daniel da Luz Mota. Coping with the reality: adding crucial features to a typestate-oriented language. Master’s thesis, Universidade Nova de Lisboa, Faculdade de Ciências e Tocnologia, February 2021.
[DMD16a] Yao Dong, Ana Milanova, and Julian Dolby. JCrypt: Towards computation over encrypted data. In PPPJ 2016: Proceedings of the 13th International Conference on Principles and Practice of Programming in Java: Virtual Machines, Languages, and Tools, Lugano, Switzerland, July 2016.
[DMD16b] Yao Dong, Ana Milanova, and Julian Dolby. Static analysis and program transformation for secure computation on the cloud. In ISSTA 2016 Doctoral Symposium, Saarbrücken, Genmany, July 2016.
[Don17] Yao Dong. Static analysis and program transformation for secure computation on the cloud. PhD thesis, Rensselaer Polytechnic Institute, December 2017.
[EJM⁺14] Michael D. Ernst, René Just, Suzanne Millstein, Werner Dietl, Stuart Pernsteiner, Franziska Roesner, Karl Koscher, Paulo Barros, Ravi Bhoraskar, Seungyeop Han, Paul Vines, and Edward X. Wu. Collaborative verification of information flow for a high-assurance app store. In CCS 2014: Proceedings of the 21st ACM Conference on Computer and Communications Security, pages 1092–1104, Scottsdale, AZ, USA, November 2014.
[ELM⁺16] Michael D. Ernst, Alberto Lovato, Damiano Macedonio, Fausto Spoto, and Javier Thaine. Locking discipline inference and checking. In ICSE 2016, Proceedings of the 38th International Conference on Software Engineering, pages 1133–1144, Austin, TX, USA, May 2016.
[EMMS16] Michael D. Ernst, Damiano Macedonio, Massimo Merro, and Fausto Spoto. Semantics for locking specifications. In NFM 2016: 8th NASA Formal Methods Symposium, pages 355–372, Minneapolis, MN, USA, June 2016.
[Ern08a] Michael D. Ernst. Building and using pluggable type systems with the Checker Framework. In ECOOP 2008 — Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 2008. Tool demo.
[Ern08b] Michael D. Ernst. Type Annotations specification (JSR 308). https://checkerframework.org/jsr308/, September 12, 2008.
[GBS13] Prodromos Gerakios, Aggelos Biboudis, and Yannis Smaragdakis. Reified type parameters using java annotations. In GPCE 2013: Proceedings of the 12th International Conference on Generative Programming and Component Engineering, pages 61–64, Indianapolis, IN, USA, October 2013.
[GDEG13] Colin S. Gordon, Werner Dietl, Michael D. Ernst, and Dan Grossman. JavaUI: Effects for controlling UI object access. In ECOOP 2013 — Object-Oriented Programming, 27th European Conference, pages 179–204, Montpellier, France, July 2013.
[Goe06] Brian Goetz. The pseudo-typedef antipattern: Extension is not type definition. https://web.archive.org/web/20171025205847/https://www.ibm.com/developerworks/java/library/j-jtp02216/, February 21, 2006.
[GPB⁺06] Brian Goetz, Tim Peierls, Joshua Bloch, Joseph Bowbeer, David Holmes, and Doug Lea. Java Concurrency in Practice. Addison-Wesley, 2006.
[GV18] Sascha Gschwind and Renato Venzin. Googletest to CUTE converter. Technical report, University of Applied Sciences Rapperswil, Rapperswil, Switzerland, 2018.
[Har10] Artemus Harper. Applying uniqueness to the Java language. Master’s thesis, Washington State University, 2010.
[HDM14] Wei Huang, Yao Dong, and Ana Milanova. Type-based taint analysis for Java web applications. In FASE 2014: Fundamental Approaches to Software Engineering, pages 140–154, Grenoble, France, April 2014.
[HDMD15] Wei Huang, Yao Dong, Ana Milanova, and Julian Dolby. Scalable and precise taint analysis for Android. In ISSTA 2015, Proceedings of the 2015 International Symposium on Software Testing and Analysis, pages 106–117, Baltimore, MD, USA, July 2015.
[HDME12] Wei Huang, Werner Dietl, Ana Milanova, and Michael D. Ernst. Inference and checking of object ownership. In ECOOP 2012 — Object-Oriented Programming, 26th European Conference, pages 181–206, Beijing, China, June 2012.
[HM11] Wei Huang and Ana Milanova. Towards effective inference and checking of ownership types. In IWACO 2011: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming, Lancaster, UK, July 2011.
[HM12] Wei Huang and Ana Milanova. ReImInfer: Method purity inference for Java. In FSE 2012: Proceedings of the ACM SIGSOFT 20th Symposium on the Foundations of Software Engineering, pages 1–4, Cary, NC, USA, November 2012.
[HMDE12] Wei Huang, Ana Milanova, Werner Dietl, and Michael D. Ernst. ReIm & ReImInfer: Checking and inference of reference immutability and method purity. In OOPSLA 2012, Object-Oriented Programming Systems, Languages, and Applications, pages 879–896, Tucson, AZ, USA, October 2012.
[HP04] David Hovemeyer and William Pugh. Finding bugs is easy. In OOPSLA Companion: Companion to Object-Oriented Programming Systems, Languages, and Applications, pages 132–136, Vancouver, BC, Canada, October 2004.
[HP09] Christian Haack and Erik Poll. Type-based object immutability with flexible initialization. In ECOOP 2009 — Object-Oriented Programming, 23rd European Conference, pages 520–545, Genova, Italy, July 2009.
[HSP05] David Hovemeyer, Jaime Spacco, and William Pugh. Evaluating and tuning a static analysis to find null pointer bugs. In PASTE 2005: ACM SIGPLAN/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2005), pages 13–19, Lisbon, Portugal, September 2005.
[Hua14] Wei Huang. An inference and checking framework for context-sensitive pluggable types. PhD thesis, Rennselaer Polytechnic Institute, 2014.
[Iri16] Karamitrou Irini. A crowdsourcing game for formal software verification. Bachelor’s thesis, University of Thessaly Polytechnic School Department of Electrical and Computer Engineering, Thessaly, Greece, 2016.
[Kai15] Benjamin Kaiser. A context-sensitive security type system for Java. Master’s thesis, Rennselaer Polytechnic Institute, Troy, NY, USA, April 2015.
[KDME18] Martin Kellogg, Vlastimil Dort, Suzanne Millstein, and Michael D. Ernst. Lightweight verification of array indexing. In ISSTA 2018, Proceedings of the 2018 International Symposium on Software Testing and Analysis, pages 3–14, Amsterdam, Netherlands, July 2018.
[Kel19] Martin Kellogg. Compile-time detection of machine image sniping. In ASE 2019: Proceedings of the 34th Annual International Conference on Automated Software Engineering, pages 1256–1258, San Diego, CA, USA, September 2019.
[Kel22] Martin Kellogg. Lightweight Verification via Specialized Typecheckers. PhD thesis, University of Washington Paul G. Allen School of Computer Science and Engineering, Seattle, WA, USA, June 2022.
[KEW⁺20] Mirko Köhler, Nafise Eskandani, Pascal Weisenburger, Alessandro Margara, and Guido Salvaneschi. Rethinking safe consistency in distributed object-oriented programming. In OOPSLA 2020, Object-Oriented Programming Systems, Languages, and Applications, Chicago, IL, USA, November 2020.
[Kog17] Alexander V. Kogtenkov. Null safety benchmarks for object initialization. Proceedings of the Institute for System Programming of RAS, 29(6):135–150, 2017.
[KRS⁺20] Martin Kellogg, Manli Ran, Manu Sridharan, Martin Schäf, and Michael D. Ernst. Verifying object construction. In ICSE 2020, Proceedings of the 42nd International Conference on Software Engineering, pages 1447–1458, Seoul, Korea, May 2020.
[KS17] Maria Kechagia and Diomidis Spinellis. Type checking for reliable APIs. In WAPI ’17: Proceedings of the 1st International Workshop on API Usage and Evolution, pages 15–18, Buenos Aires, Argentina, May 2017.
[KSSE21] Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. Lightweight and modular resource leak verification. In ESEC/FSE 2021: The ACM 29th joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 181–192, Athens, Greece, August 2021.
[KSSE22] Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. Accumulation analysis. In ECOOP 2022 — Object-Oriented Programming, 33rd European Conference, pages 10:1–10:31, Berlin, Germany, June 2022.
[KSTE20] Martin Kellogg, Martin Schäf, Serdar Tasiran, and Michael D. Ernst. Continuous compliance. In ASE 2020: Proceedings of the 35th Annual International Conference on Automated Software Engineering, pages 511–523, Melbourne, Australia, September 2020.
[Lan21] Florian Lanzinger. Property types in Java: Combining type systems and deductive verification. Master’s thesis, Karlsruher Institut für Technologie, feb 2021.
[LBOK16] Li Li, Tegawendé F. Bissyandé, Damien Octeau, and Jacques Klein. Reflection-aware static analysis of Android apps. In ASE 2016: Proceedings of the 31st Annual International Conference on Automated Software Engineering, pages 756–761, Singapore, Singapore, September 2016.
[LBR06] Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 31(3), March 2006.
[LBSD16] Shuang Liu, Guangdong Bai, Jun Sun, and J. Dong. Towards using concurrent Java API correctly. In ICECCS 2016: 21st International Conference on Engineering of Complex Computer Systems, pages 219–222, Dubai, UAE, June 2016.
[LČCT19] Tianhan Lu, Pavol Černý, Bor-Yuh Evan Chang, and Ashutosh Trivedi. Type-directed bounding of collections in reactive programs. In VMCAI 2019: 20th International Conference on Verification, Model Checking and Abstract Interpretation, pages 275–296, Cascais, Portugal, January 2019.
[Li17] Jianchu Li. A general pluggable type inference framework and its use for data-flow analysis. Master’s thesis, U. of Waterloo, Waterloo, Ontario, Canada, 2017.
[LWUD21] Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, and Werner Dietl. Scalability and precision by combining expressive type systems and deductive verification. Proceedings of the ACM on Programming Languages, 5(OOPSLA), October 2021.
[Mac16] Christopher A. Mackie. Preventing signedness errors in numerical computations in Java. In FSE 2016: Proceedings of the ACM SIGSOFT 24th Symposium on the Foundations of Software Engineering, pages 1148–1150, Seattle, WA, USA, November 2016.
[MGR21] João Mota, Marco Giunti, and António Ravara. Java typestate checker. In Coordination 2021: 23rd IFIP WG 6.1 International Conference on Coordination Models and Languages, page 121–133, Valletta, Malta, June 2021.
[MH12] Ana Milanova and Wei Huang. Inference and checking of context-sensitive pluggable types. In FSE 2012: Proceedings of the ACM SIGSOFT 20th Symposium on the Foundations of Software Engineering, pages 1–4, Cary, NC, USA, November 2012.
[MH13] Ana Milanova and Wei Huang. Composing polymorphic information flow systems with reference immutability. In FTfJP: 14th Workshop on Formal Techniques for Java-like Programs, pages 5:1–5:7, Montpellier, France, July 2013.
[MHD14] Ana Milanova, Wei Huang, and Yao Dong. CFL-reachability and context-sensitive integrity types. In PPPJ 2014: Proceedings of the 2014 International Conference on Principles and Practice of Programming in Java: Virtual Machines, Languages, and Tools, page 99–109, Cracow, Poland, September 2014.
[Mil18] Ana Milanova. Definite reference mutability. In ECOOP 2018 — Object-Oriented Programming, 32nd European Conference, pages 25:1–25:30, Amsterdam, Netherlands, July 2018.
[MV11] Ana Milanova and Jan Vitek. Static dominance inference. In TOOLS 2011: Objects, Models, Components, Patterns, 49th International Conference, pages 211–227, Zurich, Switzerland, June 2011.
[MWME21] Rashmi Mudduluru, Jason Waataja, Suzanne Millstein, and Michael D. Ernst. Verifying determinism in sequential programs. In ICSE 2021, Proceedings of the 43rd International Conference on Software Engineering, pages 37–49, Madrid, Spain, May 2021.
[Noa10] Gunther Noack. TIFI+: A type checker for object immutability with flexible initialization. Diploma thesis, University of Kaiserslautern, March 2010.
[NR19] Abel Nieto Rodriguez. Scala with explicit nulls. Master’s thesis, University of Waterloo Department of Computer Science, Waterloo, Ontario, Canada, December 2019.
[NZL⁺20] Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu. Scala with explicit nulls. In ECOOP 2020 — Object-Oriented Programming, 33rd European Conference, pages 25:1–25:26, online, November 2020.
[PAC⁺08] Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. Practical pluggable types for Java. In ISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis, pages 201–212, Seattle, WA, USA, July 2008.
[PÖZE13] Alex Potanin, Johan Östlund, Yoav Zibin, and Michael D. Ernst. Immutability. In Aliasing in Object-Oriented Programming, volume 7850 of LNCS, pages 233–269. Springer-Verlag, April 2013.
[QTE08] Jaime Quinonez, Matthew S. Tschantz, and Michael D. Ernst. Inference of reference immutability. In ECOOP 2008 — Object-Oriented Programming, 22nd European Conference, pages 616–641, Paphos, Cyprus, July 2008.
[San16] Joseph Santino. Enforcing correct array indexes with a type system. In FSE 2016: Proceedings of the ACM SIGSOFT 24th Symposium on the Foundations of Software Engineering, pages 1142–1144, Seattle, WA, USA, November 2016.
[SCN17] Julian Sexton, Andrey Chudnov, and David A. Naumann. Spartan Jester: end-to-end information flow control for hybrid Android applications. In SPW 2017: Symposium Security and Privacy Workshops, pages 157–162, San Jose, CA, USA, May 2017.
[SCSC18] Benno Stein, Lazaro Clapp, Manu Sridharan, and Bor-Yuh Evan Chang. Safe stream-based programming with refinement types. In ASE 2018: Proceedings of the 33rd Annual International Conference on Automated Software Engineering, pages 565–576, Montpellier, France, September 2018.
[SDE12] Eric Spishak, Werner Dietl, and Michael D. Ernst. A type system for regular expressions. In FTfJP: 14th Workshop on Formal Techniques for Java-like Programs, pages 20–26, Beijing, China, June 2012.
[SDF⁺11] Adrian Sampson, Werner Dietl, Emily Fortuna, Danushen Gnanapragasam, Luis Ceze, and Dan Grossman. EnerJ: Approximate data types for safe and general low-power computation. In PLDI 2011: Proceedings of the ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation, pages 164–174, San Jose, CA, USA, June 2011.
[SE10] Todd W. Schiller and Michael D. Ernst. Rethinking the economics of software engineering. In FoSER: Workshop on the Future of Software Engineering Research, pages 325–330, Santa Fe, NM, USA, November 2010.
[SE11] Fausto Spoto and Michael D. Ernst. Inference of field initialization. In ICSE 2011, Proceedings of the 33rd International Conference on Software Engineering, pages 231–240, Waikiki, Hawaii, USA, May 2011.
[SGT⁺23] Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu Lahiri, Akash Lal, and Manu Sridharan. Inference of resource management specifications. Proceedings of the ACM on Programming Languages, 7(OOPSLA2, article #282):1705–1728, October 2023.
[She11] Amanj Sherwany. The design, implementation and evaluation of a pluggable type checker for thread-locality in Java. Master’s thesis, Uppsala University, Department of Information Technology, Uppsala, Sweden, 2011.
[SM11] Alexander J. Summers and Peter Müller. Freedom before commitment: A lightweight type system for object initialisation. In OOPSLA 2011, Object-Oriented Programming Systems, Languages, and Applications, pages 1013–1032, Portland, OR, USA, October 2011.
[Spo10] F. Spoto. The nullness analyser of Julia. In LPAR 2010: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pages 405–424, Dakar, Senegal, April 2010.
[Sun21] Lian Sun. An immutability type system for classes and objects: Improvements, experiments, and comparisons. Master’s thesis, University of Waterloo Department of Electrical and Computer Engineering, Waterloo, Ontario, Canada, April 2021.
[Ta18] Mier Ta. Context sensitive typechecking and inference: Ownership and immutability. Master’s thesis, University of Waterloo Department of Electrical and Computer Engineering, Waterloo, Ontario, Canada, 2018.
[TE05] Matthew S. Tschantz and Michael D. Ernst. Javari: Adding reference immutability to Java. In OOPSLA 2005, Object-Oriented Programming Systems, Languages, and Applications, pages 211–230, San Diego, CA, USA, October 2005.
[TPNV11] Daniel Tang, Ales Plsek, Kelvin Nilsen, and Jan Vitek. A static memory safety annotation system for Safety Critical Java. In RTSS 2011: The 32nd IEEE Real-Time Systems Symposium, Vienna, Austria, November 2011.
[TPV10] Daniel Tang, Ales Plsek, and Jan Vitek. Static checking of safety critical Java annotations. In JTRES 2010: 8th International Workshop on Java Technologies for Real-time and Embedded Systems, pages 148–154, Prague, Czech Republic, August 2010.
[Val18] Lembit Valgma. Usable and sound static analysis through its integration into automated and interactive workflows. Master’s thesis, U. of Tartu, Tartu, Estonia, 2018.
[VPEJ15] Mohsen Vakilian, Amarin Phaosawasdi, Michael D. Ernst, and Ralph E. Johnson. Cascade: A universal programmer-assisted type qualifier inference tool. In ICSE 2015, Proceedings of the 37th International Conference on Software Engineering, pages 234–245, Florence, Italy, May 2015.
[Wan21] Di Wang. Interval type inference: Improvements and evaluations. Master’s thesis, University of Waterloo Department of Electrical and Computer Engineering, Waterloo, Ontario, Canada, December 2021.
[WKSE14] Konstantin Weitz, Gene Kim, Siwakorn Srisakaokul, and Michael D. Ernst. A type system for format strings. In ISSTA 2014, Proceedings of the 2014 International Symposium on Software Testing and Analysis, pages 127–137, San Jose, CA, USA, July 2014.
[WPM⁺09] Tobias Wrigstad, Filip Pizlo, Fadi Meawad, Lei Zhao, and Jan Vitek. Loci: Simple thread-locality for Java. In ECOOP 2009 — Object-Oriented Programming, 23rd European Conference, pages 445–469, Genova, Italy, July 2009.
[XCD21] Weitian Xing, Yuanhui Cheng, and Werner Dietl. Ensuring correct cryptographic algorithm and provider usage at compile time. In FTfJP: 239d Workshop on Formal Techniques for Java-like Programs, page 43–50, Online, July 2021.
[Xia20] Tongtong Xiang. Type checking and whole-program inference for value range analysis. Master’s thesis, University of Waterloo Department of Electrical and Computer Engineering, Waterloo, Ontario, Canada, October 2020.
[Xin20] Weitian Xing. Light-weight verification of cryptographic API usage. Master’s thesis, U. of Waterloo, Waterloo, Ontario, Canada, 2020.
[XLD20] Tongtong Xiang, Jeff Y. Luo, and Werner Dietl. Precise inference of expressive units of measurement types. In OOPSLA 2020, Object-Oriented Programming Systems, Languages, and Applications, Chicago, IL, USA, November 2020.
[Zaz13] Nosheen Zaza. Evaluating the accuracy of annotations in the Loci 3.0 pluggable type checker. Master’s thesis, Uppsala University, Uppsala, Sweden, 2013.
[ZPA⁺07] Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kieżun, and Michael D. Ernst. Object and reference immutability using Java generics. In ESEC/FSE 2007: Proceedings of the 11th European Software Engineering Conference and the 15th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 75–84, Dubrovnik, Croatia, September 2007.
[ZPL⁺10] Yoav Zibin, Alex Potanin, Paley Li, Mahmood Ali, and Michael D. Ernst. Ownership and immutability in generic Java. In OOPSLA 2010, Object-Oriented Programming Systems, Languages, and Applications, pages 598–617, Revo, NV, USA, October 2010.

The Checker Framework Manual: Custom pluggable types for Java