William Schultz

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

I am a staff research engineer at MongoDB, focused on distributed systems and formal methods.

I received my PhD in computer science in the formal methods group at Northeastern University where I was advised by Stavros Tripakis. Generally, my research interests are centered around the application of formal methods to the verification, design, and interpretability of distributed systems and protocols.

During my PhD I interned at Apple, working on formal verification of their hardware designs, and also at Microsoft Research, where I worked on compositional verification techniques for distributed protocols within the Azure Research group.

Prior to this I worked as a software engineer at MongoDB on their distributed replication system. Before that I was an undergraduate at Cornell University, where I studied Math and Computer Science.

Publications

  • Interpretable Safety Verification of Distributed Protocols by Inductive Proof Decomposition [draft]
    William Schultz, Edward Ashton, Heidi Howard, and Stavros Tripakis. Under Submission
  • Efficient Synthesis of Symbolic Distributed Protocols by Sketching [pdf] [code]
    Derek Egolf, William Schultz, and Stavros Tripakis. FMCAD 2024
  • Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+ [pdf] [code]
    William Schultz, Ian Dardik, and Stavros Tripakis. FMCAD 2022
  • Formal Verification of a Distributed Dynamic Reconfiguration Protocol [pdf] [code]
    William Schultz, Ian Dardik, and Stavros Tripakis. CPP 2022
  • Design And Analysis of a Logless Dynamic Reconfiguration Protocol [pdf] [full version] [code] [visualization]
    William Schultz, Siyuan Zhou, Ian Dardik, and Stavros Tripakis. OPODIS 2021
  • Tunable Consistency in MongoDB [pdf]
    William Schultz, Tess Avitabile, and Alyson Cabral. VLDB 2019

Talks

  • Interpretable Verification of Distributed Protocols by Inductive Proof Decomposition [link] [slides]
    William Schultz. CMU Software Research Seminar, Fall 2024.
  • Scalable, Interpretable Protocol Verification by Inductive Proof Slicing [link] [slides]
    William Schultz. New England Systems Verification Day 2024.
  • Towards Better Interactive Formal Specifications [video] [code]
    William Schultz. TLA+ Conference 2024.
  • Inductive Invariant Inference in TLA+ [link]
    William Schultz. New England Systems Verification Day 2022.
  • A Bug's Life: Fixing a MongoDB Replication Protocol Bug with TLA+ [video] [slides]
    William Schultz and Siyuan Zhou. TLA+ Conference 2019.

Experience

  • Summer 2023 Research Intern, Microsoft Research Cambridge
  • Spring 2023 Formal Verification Intern, Apple
  • Summer 2022 Applied Scientist Intern, Amazon Web Services (AWS)
  • Summer 2021 Research Intern, NASA Langley Research Center [presentation]
  • 2016 - 2020 Software Engineer, MongoDB