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.
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:
- 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).
- 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 19
Aug 18
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!
Aug 7
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!
Jun 11
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!
2022 Sep
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.
Papers
- On the Relationship Between Code Verifiability and Understandability
- European Software Engineering Conference/Foundations of Software Engineering (ESEC/FSE), December 2023
- [bibtex] [artifact]
- Inference of Resource Management Specifications
- Proceedings of the ACM on Programming Languages (OOPSLA), October 2023
- [bibtex] [artifact]
- Pluggable Type Inference for Free
- 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
- PhD Thesis, University of Washington, Seattle, USA, June 2022
- [bibtex]
- Lightweight Verification via Specialized Typecheckers
- 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
- 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
- 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 2023: CS 490: Guided Design in Software EngineeringSpring 2023: CS 490: Guided Design in Software Engineering
Fall 2022: CS 785: Practical Program Analysis
PhD Students
Kazi Amanul Islam Siddiqui, 2023-presentErfan Arvan, 2023-present
Professional Service
Sponsorship Chair, SPLASH 2024Program 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