---

2024

“Nullness Checker Test Suite Improvements”
by Charlie Cao.
May 2024. Spring 2024 undergraduate volunteer (ongoing).
Details.

“JSpecify Conformance Test Improvements”
by Haibo Sun.
May 2024. Spring 2024 URA student (ongoing).
Details.

“Design and Implementation of a Type System for Enhanced Mathematical Operations in Rings”
by Yuliia Nortman.
May 2024. PhD exchange student (ongoing).
Details.

“JSpecify conformance tests for the EISOP Nullness Checker”
by Rohan Shetty.
Apr. 2024. Winter 2024 URA student (started January 2024).
Details.

“Build system integration improvements”
by Omer Adeel.
Apr. 2024. Winter 2024 URA student (started January 2024).
Details.

“Basic support for SARIF file format”
by Shaheer Hasan.
Apr. 2024. Winter 2024 URA student (started January 2024).
Details.

“Avoiding bytecode storage for optional type systems”
by Emily Tao.
Apr. 2024. Winter 2024 URA student (started January 2024).
Details.

2023

“Integrate type system knowledge into the ECF language server”
by Zain Salman.
Dec. 2023. Fall 2023 URA student (started September 2023).
Details.

“Improved nullness analysis in the ECF language server”
by Nicholas Chew.
Dec. 2023. Fall 2023 URA student (started September 2023).
Details.

“Context-Sensitive Optional Type Systems Meet Generics: A Uniform Treatment and Formalization”
by Haifeng Shi.
Dec. 2023. MASc student (started January 2022).
Details.

“A Lightweight Type System with Uniqueness and Typestates for the Java Cryptography API”
by Alex Liu.
Aug. 2023. MASc student (started January 2022).
Details.

“Optional type systems for database queries”
by Thomas Kirz.
June 2023. MASc student (ongoing) now at TU Wien; collaboration with Prof. Scherzinger, University of Passau, and Mattias Ulbrich, KIT.
Details.

“Improved Abstractions for Deductive Proofs”
by Wolfram Pfeifer.
June 2023. PhD student (ongoing) at KIT, supervised by Mattias Ulbrich.
Details.

“UniFlow: A CFG-Based Framework for Pluggable Type Checking and Type Inference”
by Zhiping Cai.
Apr. 2023. MASc student (started May 2021); previously Winter 2020 URA student working on Checker Framework Inference Improvements (January to April 2020).
Details.

“Static Verification of 5G-AKA”
by Negar Sabour.
Apr. 2023. MASc student (started January 2022); co-supervised with Mahesh V. Tripunitara.
Details.

“JSpecify nullness specification and checker”
by Tony Sun.
Apr. 2023. Winter 2023 URA student (started January 2023).
Details.

“Interactive CFG visualization”
by Farzan Mirshekari.
Apr. 2023. Winter 2023 URA student (started January 2023).
Details.

“Automatically generating a website from GitHub releases”
by Luc Antony Lorand Edes.
Apr. 2023. Winter 2023 URA student (started January 2023).
Details.

“Pluggable Type Systems (TBD)”
by Aosen Xiong.
Jan. 2023. PhD student (ongoing).
Details.

2022

“Upgraded Live Demo Website”
by Padena Rasouli-Baghban.
Dec. 2022. Fall 2022 URA student (started September 2022).
Details.

“Type systems for Program Verification”
by Yuyan Bao.
Dec. 2022. Post-Doctoral researcher (started January 2021); co-supervised with Arie Gurfinkel. Now an Assistant Professor at Augusta University.
Details.

“OppropBERT: An Extensible Graph Neural Network and BERT-style Reinforcement Learning-based Type Inference System”
by Piyush Jha.
Dec. 2022. MASc student (started May 2021).
Details.

“Build support for multiple Java versions”
by Daniel Zhu.
Dec. 2022. Fall 2022 URA student (started September 2022).
Details.

“Website generation tool”
by Kaihang Jiang.
Aug. 2022. Spring 2022 URA student (started May 2022).
Details.

“Test case generation tool”
by Javier Rodriguez.
Aug. 2022. Spring 2022 URA student (started May 2022).
Details.

“Project documentation and improvements”
by Fady Abousifein.
Aug. 2022. Spring 2022 high school volunteer (started May 2022).
Details.

“Project documentation and improvements”
by Seung Whan (Peter) Song.
June 2022. Fall 2021/Winter 2022 high school volunteer (started September 2021).
Details.

“Preprocessing for multi-release JAR files”
by Yumeng Chen.
Apr. 2022. Winter 2022 URA student (started January 2022).
Details.

2021

“Multi-release JAR files for compiler plug-ins”
by Jing Liu.
Dec. 2021. Fall 2021 URA student (started September 2021).
Details.

“Interval Type Inference: Improvements and Evaluations”
by Di Wang.
Dec. 2021. MASc student (started May 2020).
Details.

“VSCode Annotated Type Visualization”
by Evette Madeline Chan-Lee.
Aug. 2021. Spring 2021 URA student (started May 2021).
Details.

“Benchmarking and Improving Value Inference”
by Andrew Guo.
Aug. 2021. Spring 2021 URA student (started May 2021).
Details.

“Type Inference Live Demo Website”
by Willa Kong.
Apr. 2021. Winter 2021 URA student (started January 2021).
Details.

“Live Demo Website Improvements”
by Jainish Mehta.
Apr. 2021. Winter 2021 URA student (started January 2021).
Details.

“An Immutability Type System for Classes and Objects: Improvements, Experiments, and Comparisons”
by Lian Sun.
Apr. 2021. MASc student (started September 2019). Previously MEng student assistant in Spring 2019.
Details.

“Object Capability Systems (TBD)”
by Mark S. Dittmer.
Jan. 2021. PhD student (ongoing); co-supervised with Mahesh V. Tripunitara.
Details.

2020

“Type Inference Benchmarks”
by Frank Ding.
Dec. 2020. Fall 2020 URA student (started September 2020).
Details.

“Light-weight verification of cryptographic API usage”
by Weitian Xing.
Dec. 2020. MASc student (started May 2019). Previously MEng student assistant in Winter 2019.
Details.

“Least-Privilege Identity-Based Policies for Lambda Functions in Amazon Web Services (AWS)”
by Puneet Gill.
Dec. 2020. MASc student (started January 2019); co-supervised with Mahesh V. Tripunitara.
Details.

“Type Checking and Whole-program Inference for Value Range Analysis”
by Jenny (Tongtong) Xiang.
Oct. 2020. MASc student (started May 2018). Spring 2019: Internship at Amazon Web Services in Seattle, USA.
Details.

“General Tainting Checker”
by Aditya Singh.
Sep. 2020. Spring 2020 GSoC student (started May 2020). Google Summer of Code (GSoC) is a competitive intern funding program from Google. Dr. Dietl is one of the GSoC organizers for the Checker Framework project and is the GSoC advisor for Mr. Singh.
Details.

“Improving Viewpoint Adaptation Test Coverage”
by Leo Liu.
Aug. 2020. Spring 2020 URA student (started May 2020).
Details.

“Checker Framework IDE Integration”
by Shiji Liu.
Aug. 2020. Spring 2020 URA student (started May 2020).
Details.

“Property Type Systems”
by Florian Lanzinger.
May 2020. Visiting PhD student (September to November 2022); PhD student at KIT, supervised by Mattias Ulbrich; previously MASc student, co-advised with Mattias Ulbrich, KIT (May 2020 to February 2021).
Details.

“Correct Usage of Cryptographic APIs”
by Yuanhui Cheng.
Apr. 2020. Winter 2020 URA student (started January 2020).
Details.

“Checker Framework Live Demo Website Improvements”
by Ahmad Tahir Chaudhry.
Apr. 2020. Winter 2020 student volunteer (started January 2020).
Details.

“Checker Framework Eclipse Integration”
by Hejia Wang.
Apr. 2020. Winter 2020 URA student (started January 2020).
Details.

2019

“Pluggable Type Systems”
by Jeff Luo.
Dec. 2019. PhD student (started July 2014, incomplete). Spring 2016 and Spring 2017: Internships at Google, Waterloo, Canada. Mr. Luo was awarded scholarships, including two Queen Elizabeth II Graduate Scholarships in Science & Technology, and awards for his excellent teaching efforts. On leave January to December 2019, terminated PhD program in December 2019. Now at Google.
Details.

“Performance of Static Analysis Systems”
by Nhat Nguyen.
Dec. 2019. Fall 2019 CS 499R student (started September 2019).
Details.

“Checker Framework LSP Server”
by Jiangqi Zhang.
Dec. 2019. ECE 699 and MEng student assistant (started January 2019).
Details.

“Checker Framework Eclipse Integration”
by Michael Xiheng Jiang.
Dec. 2019. Fall 2019 URA student (started September 2019).
Details.

“Android Support Annotations”
by Ayush Agarwal.
Aug. 2019. Spring 2019 GSoC student (started April 2019). Google Summer of Code (GSoC) is a competitive intern funding program from Google. Dr. Dietl is one of the GSoC organizers for the Checker Framework project and was the GSoC advisor for Mr. Agarwal.
Details.

“Pluggable Type System Formalizations”
by Baorui Zhou.
Apr. 2019. Winter 2019 URI student, Fall 2018 URA student, Spring 2018 URI student.
Details.

2018

“GoA — Actors with Locally Managed Memory for Go”
by Daniel Gerald Caccamo.
Dec. 2018. MASc student (started September 2016). Spring 2017: Internship at Amazon, Seattle, USA. Now at IBM, Ottawa, Canada.
Details.

“Gauss-Jordan Constraint Solver”
by Sunjay Varma.
Dec. 2018. Fall 2018 URA student (started September 2018).
Details.

“Checker Framework Inference Web Demo”
by Jerry Huang.
Dec. 2018. Fall 2018 URA student (started September 2018).
Details.

“Checker Framework Atom Integration”
by Yiren Zhou.
Dec. 2018. Fall 2018 URA student (started September 2018).
Details.

“Checker Framework LSP Integration”
by Adam Yifan Yang.
Aug. 2018. Spring 2018 URA student (started May 2018).
Details.

“Checker Framework Java 9 support”
by Ravi Roshan.
Aug. 2018. Spring 2018 GSoC student (started April 2018). Google Summer of Code (GSoC) is a competitive intern funding program from Google. Dr. Dietl is one of the GSoC organizers for the Checker Framework project and was the GSoC advisor for Mr. Roshan.
Details.

“Pluggable Type Systems”
by Sadaf Tajik.
Apr. 2018. MASc student (started September 2017, not finished).
Details.

“Pluggable Properties for Program Understanding: Ontic Type Checking and Inference”
by Charles Zhuo Chen.
Apr. 2018. MASc student (started January 2016). Winter 2017: Internship at Amazon, Toronto, Canada. Now a full-time employee there.
Details.

“Context Sensitive Typechecking And Inference: Ownership And Immutability”
by Mier Ta.
Apr. 2018. MASc student (started January 2016). Winter 2017: Internship at Amazon, Vancouver, Canada. Now a full-time employee at Amazon, Toronto, Canada.
Details.

“Checker Framework VSCode Integration”
by Amanda Yuxin Jiang.
Apr. 2018. Winter 2018 URA student (started January 2018).
Details.

2017

“Checker Framework IDE Integration”
by Haaris Ahmed.
Dec. 2017. Fall 2017 URA student (started September 2017).
Details.

“Control Flow Graph Enhancements”
by Shinya Yoshida.
Aug. 2017. Spring 2017 GSoC student (started April 2017). Google Summer of Code (GSoC) is a competitive intern funding program from Google. Dr. Dietl is one of the GSoC organizers for the Checker Framework project and was the GSoC advisor for Mr. Yoshida.
Details.

“Checker Framework Live Demo Improvements”
by Boying (Ashley) Liu.
Aug. 2017. Spring 2017 URA student (started May 2017).
Details.

“Benchmark infrastructure and Web Interface”
by Vic Hao-Chien Lin.
Aug. 2017. Spring 2017 USRA student (started May 2017).
Details.

“A General Pluggable Type Inference Framework and its use for Data-flow Analysis”
by Jason Jianchu Li.
Apr. 2017. MASc student (started May 2015). Spring 2016: Internship at Blackberry, Waterloo, Canada. Now at Amazon, Vancouver, Canada.
Details.

2016

“Investigate a new Pluggable Type System”
by Andy Chang Ho Lee.
Dec. 2016. Fall 2016 URA student (started September 2016).
Details.

“Checker Framework Rise4Fun Integration”
by Fernando Peña.
Dec. 2016. Fall 2016 URA student (started September 2016).
Details.

“Checker Framework Performance Improvements”
by Thomas Feng.
Dec. 2016. Fall 2016 student volunteer (started September 2016).
Details.

“Checker Framework NetBeans Integration”
by Tony Rong Tan Wang.
Dec. 2016. Fall 2016 URA student (started September 2016).
Details.

“Checker Framework Java~9 Update”
by Matthew D'Souza.
Dec. 2016. Fall 2016 URA student (started September 2016).
Details.

“Checker Framework IntelliJ Integration”
by Steven Jia.
Dec. 2016. Fall 2016 URA student (started September 2016).
Details.

“Checker Framework Inference Improvements”
by Luqman Aden.
Dec. 2016. Fall 2016 USRA student (started September 2016). Now at Microsoft, Redmond, USA.
Details.

“Pluggable Type Systems”
by Yameng Li.
July 2016. MEng student volunteer (started May 2016).
Details.

“Checker Framework Performance Profiling”
by Shruti Dembla.
May 2016. Winter 2016 URA student (started January 2016).
Details.

“Gradual Pluggable Typing in Java”
by Dan Brotherston.
Apr. 2016. MMath student (started May 2014); co-supervised with Ondrej Lhoták. Now at TL Innovation Lab, Waterloo, Canada.
Details.

2015

“Complexity Analysis of Tunable Static Inference For Generic Universe Types”
by Nahid Juma.
Aug. 2015. MASc student (started July 2014); co-supervised with Mahesh V. Tripunitara.
Details.

2013

“Verification games: graph description and layout; game generation”
by Nathaniel Mote.
Oct. 2013. Undergraduate research (started January 2011). Now at Facebook, Washington, USA.
Details.

“Verification games: extended type systems; game generation”
by Tyler Rigsby.
Oct. 2013. Undergraduate research (started March 2012). Now at Google, California, USA.
Details.

“SPARTA: case studies and extensions”
by Philip Lai.
Oct. 2013. Undergraduate research (started June 2012). Now at Indeed.com.
Details.

“Units-of-Measurement type system”
by Eric Reed.
Oct. 2013. PhD student (started September 2012).
Details.

“String format type system”
by Konstantin Weitz.
Oct. 2013. PhD student (started February 2013). Now at Google, California, USA.
Details.

“Qualifier polymorphic type systems”
by Stuart A. Pernsteiner.
Oct. 2013. PhD student (started September 2012).
Details.

“Improved dataflow analysis for the Checker Framework”
by Stefan Heule.
July 2013. Undergraduate and Master's research (started September 2011). Now at Google, California, USA.
Details.

“Interning type checker case studies; verification games: KeyFor integration; testing framework”
by Stephanie Dietzel.
Apr. 2013. Undergraduate and Master's research (started July 2011). Now at Tableau Software.
Details.

“Fake enumerations and regular expression type checker case studies and extensions; verification games: annotation and cast handling”
by Eric Spishak.
Apr. 2013. Undergraduate and Master's research (started April 2011). Now at Google, California, USA.
Details.

“Verification games: website integration”
by Brian Walker.
Jan. 2013. Undergraduate research (started January 2012). Now at Google, California, USA.
Details.

2012

“Fake enumerations and nullness type checker case study on the OpenJDK javac”
by Mark Davis.
July 2012. Undergraduate research (started July 2011).
Details.

2011

“Evaluating Practical Non-Null Type Systems for Java”
by Dimitrios C. Gklezakos, Stefan Heule, and Brandon Holt.
Dec. 2011. CSE 503 course project.
Details.

2010

“Dataflow support for the Checker Framework”
by Andreas Abel, Kivanc Muslu, and Brandon Myers.
Dec. 2010. CSE 501 course project.
Details.

2008

“A Universe Type Checker using JSR308”
by Phokham Nonava.
Sep. 2008. Semester project.
Details.

“Implementing a Universe Type Checker in Scala”
by Manfred Stock.
Jan. 2008. Master's thesis.
Details. Download: PDF.

2007

“Visualizer for Universe Type Inference Information”
by Timur Erdag.
Sep. 2007. Semester project.
Details.

“Runtime Support for Generics and Transfer in Universe Types”
by Mathias Ottiger.
Aug. 2007. Master's thesis, co-supervised with A. Rudich.
Details. Download: PDF.

“Generic Universe Types in JML”
by Robin Züger.
July 2007. Master's thesis.
Details. Download: PDF.

“Universe Type System for Scala”
by Daniel Schregenberger.
June 2007. Master's thesis.
Details. Download: PDF.

“An Isabelle Formalization of the Universe Type System”
by Martin Klebermaß.
Apr. 2007. Master's thesis, co-supervised with Prof. T. Nipkow, T. U. München.
Details. Download: PDF.

“Testing Tool for Compilers”
by Dominique Schneider.
Mar. 2007. Semester project.
Details. Download: PDF.

“Combining Runtime and Static Universe Type Inference”
by Andreas Fürer.
Mar. 2007. Master's thesis.
Details. Download: PDF.

2006

“Universe Type System for Eiffel”
by Annetta Schaad.
Oct. 2006. Semester project.
Details. Download: PDF.

“MultiJava, JML, and Generics”
by Ovidio Mallo.
Oct. 2006. Semester project.
Details. Download: PDF.

“Integration of Universe Type System Tools into Eclipse”
by Paolo Bazzi.
Oct. 2006. Semester project.
Details. Download: PDF.

“Static Universe Type Inference using a SAT-Solver”
by Matthias Niklaus.
June 2006. Master's thesis.
Details. Download: PDF.

“Practical Runtime Universe Type Inference”
by Marco Bär.
May 2006. Master's thesis.
Details. Download: PDF.

“Ownership in Design Patterns”
by Stefan Nägeli.
Mar. 2006. Master's thesis.
Details. Download: PDF.

“Interaction with Ownership Graphs”
by Marco Meyer.
Mar. 2006. Semester project.
Details. Download: PDF.

“Implementing Purity and Side Effect Analysis for Java Programs”
by David Graf.
Mar. 2006. Semester project.
Details. Download: PDF.

2005

“Static Universe Type Inference”
by Nathalie Kellenberger.
Oct. 2005. Master's thesis.
Details. Download: PDF.

“Implementation of a Universe type checker in ESC/Java2”
by Dirk Wellenzohn.
Oct. 2005. Semester project.
Details. Download: PDF.

“Runtime Universe Type Inference”
by Frank Lyner.
July 2005. Master's thesis.
Details. Download: PDF.

“Bytecode support for the Universe type system and compiler”
by Alex Suzuki.
Mar. 2005. Semester project.
Details. Download: PDF.

“Applying the Universe Type System to an Industrial Application”
by Thomas Hächler.
Mar. 2005. Master's thesis.
Details. Download: PDF.

2004

“Dynamic Typechecking in the Universe Type System”
by Daniel Schregenberger.
Oct. 2004. Semester project.
Details. Download: PDF.

“Testcases for the Universe type system compiler”
by Yann Müller.
Sep. 2004. Project assistant.
Details.

“Static Fields in the Universe Type System”
by Thomas Hächler.
July 2004. Semester project.
Details. Download: PDF.

---

---