William Schultz

schultz (dot) w (at) northeastern (dot) edu

I am a third-year PhD student in the formal methods group at Northeastern University where I am advised by Prof. Stavros Tripakis. My research interests are broadly focused on automated formal verification of distributed systems.

Previously I worked as a software engineer at MongoDB on their distributed database replication system. Before that I attended Cornell University, where I studied Math and Computer Science and graduated in 2016.


B.A. Mathematics and Computer Science, May 2016
Cornell University, Ithaca, NY


Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
William Schultz, Ian Dardik, and Stavros Tripakis.
Accepted for publication at FMCAD 2022.
[pdf] [code]

Formal Verification of a Distributed Dynamic Reconfiguration Protocol
William Schultz, Ian Dardik, and Stavros Tripakis. CPP 2022
[code] [video]

Design And Analysis of a Logless Dynamic Reconfiguration Protocol
William Schultz, Siyuan Zhou, Ian Dardik, and Stavros Tripakis. OPODIS 2021
[full version] [code] [video] [protocol visualization]

Tunable Consistency in MongoDB
William Schultz, Tess Avitabile, and Alyson Cabral. VLDB 2019


A Bug's Life: Fixing a MongoDB Replication Protocol Bug with TLA+
William Schultz and Siyuan Zhou.
Talk at TLA+ Conference 2019.
[video] [slides]

An Animation Module for TLA+
William Schultz.
Talk at TLA+ Community Event 2018.
[video] [slides]


Applied Scientist Intern, Amazon Web Services (AWS)
New York, NY
Summer 2022

Research Intern, NASA Langley Research Center
Cambridge, MA (Remote)
Summer 2021
[exit presentation]

Software Engineer, MongoDB
New York, NY
2016 - 2020