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. I am actively recruiting students to join me at NJIT: please contact me directly via email if you are interested.

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 am actively recruiting students at all levels (undergraduate, masters, PhD) to work with me beginning immediately. If the vision of making verification something that all programmers can use appeals to you, please contact me directly (email is best) or apply to NJIT and mention my name in your statement of purpose.

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

Sep 1

I’ve started my new job as an assistant professor at NJIT. I’m excited for this new chapter in my academic journey. If you’re nearby, come by and see me at my new office: GITC 4314.

Jun 3

I successfully defended my dissertation! Thanks to my committee: Rene Just, Zach Tatlock, Martin Schaef, and Nic Weber; and especially to the committee chair (and my advisor): Michael Ernst. I’m grateful for all of your great feedback and advice!

May 13

Our paper “Accumulation Analysis” was accepted at ECOOP!

Mar 1

I’ve accepted a tenure-track assistant professor position at the New Jersey Institute of Technology’s Department of Computer Science, starting in Fall 2022. I’m looking forward to the move to Newark and the next phase of my career!

Feb 22

I (virtually) gave an invited talk at George Mason University.

Feb 11

I gave an invited talk at the New Jersey Institute of Technology.

Jan 27

I (virtually) gave an invited talk at SRI.

Jan 20

I (virtually) gave an invited talk at William and Mary.

2021 Sep

We have updated our paper “Lightweight and Modular Resource Leak Verification” to correct a minor error in table 3 (the ablation study, section 7.2) that resulted from an error we discovered in our experimental scripts. None of our scientific conclusions have changed because of this correction, so the paper’s text is unchanged. The original version can still be found here.

2021 Aug

ESEC/FSE 2021 starts today! I’m participating in two talks: a doctoral symposium talk at 7am Pacific on Tuesday 8/24 and a joint talk with Narges Shadab of UCR in the main technical track on our paper “Lightweight and Modular Resource Leak Verification”, which will show twice: at 6am and 6pm Pacific time on 8/26.

2021 Jun

The pre-print of our paper “Lightweight and Modular Resource Leak Verification” (which will be published in August at ESEC/FSE) is now available.

2021 May

Our paper “Lightweight and Modular Resource Leak Verification” was accepted at ESEC/FSE 2021! Pre-print coming soon!

2020 Aug

Our paper “Continuous Compliance” was accepted at ASE 2020!

2020 Jun

I passed my general exam, meaning that I am now officially a Ph.D. candidate! Thanks to my whole committee for your excellent suggestions :)

2020 Feb

I gave a talk at the University of Utah to Pavel Panchekha’s lab.

2020 Feb

Our paper “Verifying Object Construction” was accepted at ICSE 2020’s technical track!

2019 Nov

“Compile-time Detection of Machine Image Sniping” won first place at the ASE student research competition!

2019 Sep

I’m excited to rejoin the AWS Automated Reasoning Group for an internship this fall!

2019 Aug

I updated my website!

Papers

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
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

Fall 2022: CS 785: Practical Program Analysis