I’m an assistant professor at the New Jersey Institute of Technology, in the Department of Computer Science. You can find me most days in my office: GITC 4314; feel free to come by any time that my calendar says that I’m free.

My research focuses on making software verification practical for every developer: that is, on making verification a standard part of every developer’s toolkit, in the way that techniques like unit testing or code review are today. My focus is primarily on two approaches to making verification more practical:

  1. improving the expressivity of simple verification technologies: making it possible to prove more facts about a program within the constraints that developers actually work under. Examples of this approach include my work on accumulation analysis for resource leaks (ESEC/FSE 2021) and for initialization (ICSE 2020).
  2. convincing developers of the benefits of verification: by deploying verification technologies in new domains, and by improving the usability of verification. An example of this approach is my work on compliance verification (ASE 2020).

I completed my Ph.D. at the University of Washington Paul G. Allen School of Computer Science & Engineering. I worked in the PLSE group under the supervision of Michael Ernst.

Outside of work, I enjoy playing all kinds of games—video, tabletop, board, etc.—skiing, watching baseball and soccer, reading, and a little bit of tea snobbery. Some of my favorite games include Civilization, Dungeons and Dragons, and Dominion. I’m a big fan of the Washington Nationals and of the Seattle Sounders.

I’ve made my academic job market materials publicly available: CV Research statement Teaching statement Diversity and Inclusion statement Job Talk: “Verification for working developers”

News

2023 Dec

I’m giving a talk today at ESEC/FSE in San Fransisco on our paper “On the Relationship Between Code Verifiability and Understandability” (joint work with Oscar Chaparro and his student Kobi Feldman at William and Mary) in the Empirical Studies I session (at 14:30). Slides available here.

2023 Sep

I’m thrilled that our paper “Inference of Resource Management Specifications” will appear at OOPSLA in October! This is joint work between the original Resource Leak Checker team (FSE ‘21) and folks at Microsoft Research who have implemented an RLC-inspired system for C#; we joined forces to solve the tricky inference problems that resource leak checking brings up.

2023 Aug

I’m excited that our paper “Pluggable Type Inference for Free” with my students Daniel, Loi, and Muyeed and our collaborator Michael Ernst has been accepted at ASE! Looking forward to seeing everyone in Luxembourg in September!

2023 Aug

I’m excited that my paper “On the Relationship Between Code Verifiability and Understandability” with Kobi Feldman and Oscar Chaparro has been accepted at ESEC/FSE! See you in San Fransisco in December!

2023 Jun

I’m honored that the NSF has funded my grant with Manu Sridharan to work on better type inference systems for pluggable types. I’m excited to build new inference systems that will make it easier for developers to apply pluggable typecheckers to their legacy codebases!

Papers

On the Relationship Between Code Verifiability and Understandability
European Software Engineering Conference/Foundations of Software Engineering (ESEC/FSE), December 2023
[bibtex] [artifact] [slides] [talk video]
Inference of Resource Management Specifications
Proceedings of the ACM on Programming Languages (OOPSLA), October 2023
[bibtex] [artifact]
Pluggable Type Inference for Free
  • Martin Kellogg
  • Daniel Daskiewicz
  • Loi Ngo Duc Nguyen
  • Muyeed Ahmed
  • Michael D. Ernst
Automated Software Engineering (ASE), September 2023
[bibtex] [scripts and data] [slides] [implementation]
Accumulation Analysis
European Conference on Object-Oriented Programming (ECOOP), June 2022
[bibtex] [artifact (data for literature survey)] [slides (pdf)] [slides (pptx)]
Lightweight Verification via Specialized Typecheckers
  • Martin Kellogg
PhD Thesis, University of Washington, Seattle, USA, June 2022
[bibtex]
Lightweight Verification via Specialized Typecheckers
  • Martin Kellogg
doctoral symposium at ESEC/FSE 2021, August 2021
[bibtex] [slides]
Lightweight and Modular Resource Leak Verification
European Software Engineering Conference/Foundations of Software Engineering (ESEC/FSE), August 2021
(note that this version of the paper has been updated to correct a minor error in table 3)
[bibtex] [artifact (scripts and data)] [slides (pdf)] [talk recording]
Continuous Compliance
Automated Software Engineering (ASE), August 2020
[bibtex] [artifact (scripts and data)] [slides (pdf)] [slides (pptx)] [key-length checker] [crypto-policy checker] [bucket-compliance checker] [no-literal checker]
Verifying Object Construction
International Conference on Software Engineering (ICSE), May 2020
[bibtex] [code] [artifact (VM image)] [talk video] [slides (pdf)] [slides (pptx)]
Compile-time Detection of Machine Image Sniping
  • Martin Kellogg
ASE 2019 Student Research Competition, Graduate Division, November 2019
Won 1st place at ASE ‘19’s Student Research Competition
[bibtex] [slides (PDF)] [poster (PDF)]
Lightweight Verification of Array Indexing
Internation Symposium on Software Testing and Analysis (ISSTA), July 2018
[bibtex] [slides (PDF)] [slides (PPTX)] [artifact] [docker image]
Combining Bug Detection and Test Case Generation
  • Martin Kellogg
FSE 2016 Student Research Competition, Undergraduate Division, November 2016
Won 1st place at FSE ‘16 and 3rd place in the SRC Grand Finals
[bibtex]
Combining Bug Detection and Test Case Generation
Technical Report, September 2016
[bibtex]

Teaching

Spring 2024: CS 684: Testing and Quality Assurance
Fall 2023: CS 490: Guided Design in Software Engineering
Spring 2023: CS 490: Guided Design in Software Engineering
Fall 2022: CS 785: Practical Program Analysis

PhD Students

Kazi Amanul Islam Siddiqui, 2023-present
Erfan Arvan, 2023-present

Professional Service

Sponsorship Chair, SPLASH 2024
Program Committee member, ISSTA 2023-24
Student Research Competition judge, ESEC/FSE 2023
Co-chair for Student Volunteers, ISSTA 2023
Student Research Competition judge, PLDI 2023
External Review Committee member, OOPSLA 2022-23
Artifact Evaluation Committee member, PLDI 2020
Program Committee member, testing tools track, ICST 2020
Artifact Evaluation Committee member, VMCAI 2020

Funding

Collaborative Research: SHF: MEDIUM: General and Scalable Pluggable Type Inference
$900,000 from the NSF CCF over 4 years (my share $450,000), June 2023