Checker Framework

Mentors: Student: Abhijit Kulkarni

I propose to develop NullnessLight, a lightweight, easy-to-use nullness checker built on the Checker Framework. NullnessLight will trade full soundness for usability and speed, helping developers catch common null-related bugs without requiring extensive annotations or setup. Inspired by tools like NullAway, NullnessLight will disable some of the more complex features of the existing Nullness Checker, such as initialization analysis and alias invalidation, and provide user-configurable options for these trade-offs. This project will broaden the Checker Framework's usability spectrum and help users gradually adopt deeper verification. Deliverables include the implementation of NullnessLight, a suite of comparisons with existing checkers (e.g., NullAway, FindBugs), and documentation with usage recommendations.

Mentors: Student: Damika Anupama Nanayakkara

This project aims to enhance the Checker Framework by introducing a Mutable Index Checker, which provides compile-time guarantees of index safety for dynamically sized data structures such as ArrayList, LinkedList, and Deque. Unlike the current Index Checker, which focuses on fixed-length structures like arrays and strings, this checker will track collection size changes across mutations, enabling flow-sensitive reasoning and validation of index accesses. The checker will support annotations like @IndexFor, @LengthOf, @SameLen, and custom subtyping rules to enforce both lower and upper bounds on index values. It will also provide support for aliasing-aware length consistency, post-mutation invalidation, and integration with purity annotations. Deliverables include: - A new pluggable type checker integrated into the Checker Framework. - Support for standard mutable collections with annotated APIs. - Type qualifiers and subtyping rules for index tracking. - Flow-sensitive analysis and invalidation logic on mutations. - Real-world examples, documentation, and a case study on annotating existing codebases. This tool will help developers prevent IndexOutOfBoundsException in mutable structures by enforcing correctness at compile-time—making Java applications safer and more robust.

Mentors: Student: Aditya Singh

<p>The Tainted Checker Overhaul aims to be an extension of the Tainted Checker Framework, extending the concept of tainted data and upgrading its functionalities. Often, programs need to deal with input values outside of their domain, which can sometimes allow the entry of invalidated and corrupt data. Such corrupt inputs can cause numerous errors and, therefore, must be handled carefully. This Overhaul aims to deal with such dilemmas and aid the programmer in a significant way.</p>

Mentors: Student: Priti Chattopadhyay

<p>Checker framework is a great lightweight tool which could easily type check code having a dependency on a library if the library has already been annotated. Google Gson is a widely used library written in java to transform the Java objects to JSON (JavaScript Object Notation) and vice versa. This library has a total of 143 directories and 255 files out of which 208 are java files. This project could be an overall evaluation of the type-checkers on real code and can also help detect bugs or suggest improvements to the library being annotated. The main goal of the project</p> <ol> <li>Adding annotations to the Google Gson library for Nullness, Index and Interning checker.</li> <li>Adding missing annotations in JDK and reporting bugs if found any in the process.</li> </ol>

Mentors: Student: the1derer

<p>As seen on Bazel’s <a href="https://github.com/bazelbuild/bazel/issues?utf8=%E2%9C%93&amp;q=is%3Aissue+is%3Aopen+NullPointerException+" target="_blank">Issue Page</a>, Bazel suffers from numerous <code>NullPointerException</code>( NPE ). These NPEs come out at runtime as <code>RuntimeException</code> causing a crash at runtime this leads to a large number of Issues being generated. This could be a result of not handling possible <code>null</code> values not being handled in many cases or outright poor design choices(as seen in many issues due to not handling <code>null</code> OR empty string as arguments while using certain flags).</p> <p><strong>Checker Framework's Nullness Checker</strong> runs as a compiler plug-in, and it issues a warning at every possible null pointer dereference. If it issues no warnings, the code is guaranteed not to throw a <code>NullPointerException</code> at run time.</p> <p>My project will ensure the significant reduction of these NullPointerException(s) before they happen (by checking them at compile time) rather than relying on users to report them and fixing them.</p>