Publications

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation or the Defense Advanced Research Projects Agency.
If layering is useful, why not sublayering?  (HotNets 2024)
       Rathin Singha, Rishabh Iyer, Charles Liu, Caleb Terrill, Todd Millstein, Scott Shenker, George Varghese

Bit Blasting Probabilistic Programs  (PLDI 2024)
       Poorva Garg, Steven Holtzen, Guy Van den Broeck, Todd Millstein

MESSI: Behavioral Testing of BGP Implementations  (NSDI 2024)
       Rathin Singha, Rajdeep Mondal, Ryan Beckett, Siva Kesava Reddy Kakarla, Todd Millstein, George Varghese

What do LLMs need to Synthesize Correct Router Configurations?  (HotNets 2023)
       Rajdeep Mondal, Alan Tang, Ryan Beckett, Todd Millstein, George Varghese

Lessons from the evolution of the Batfish configuration analysis tool  (SIGCOMM 2023)
       Matt Brown, Ari Fogel, Daniel Halperin, Victor Heorhiadi, Ratul Mahajan, Todd Millstein

Lightyear: Using Modularity to Scale BGP Control Plane Verification  (SIGCOMM 2023)
       Alan Tang, Ryan Beckett, Steven Benaloh, Karthick Jayaraman, Tejas Patil, Todd Millstein, George Varghese

Scaling Integer Arithmetic in Probabilistic Programs  (UAI 2023)
       William X. Cao, Poorva Garg, Ryan Tjoa, Steven Holtzen, Todd Millstein, Guy Van den Broeck

Data-Driven Lemma Synthesis for Interactive Proofs  (OOPSLA 2022)
       Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, Todd Millstein

SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers  (NSDI 2022, Applied Networking Research Prize)
       Siva Kesava Reddy Kakarla, Ryan Beckett, Todd Millstein, George Varghese

How Complex is DNS?  (HotNets 2021)
       Siva Kesava Reddy Kakarla, Ryan Beckett, Todd Millstein, George Varghese

Safe-by-default Concurrency for Modern Programming Languages  (TOPLAS)
       Lun Liu, Todd Millstein, Madanlal Musuvathi

Campion: Debugging Router Configuration Differences  (SIGCOMM 2021)
       Alan Tang, Siva Kesava Reddy Kakarla, Ryan Beckett, Ennan Zhai, Matt Brown, Todd Millstein, Yuval Tamir, George Varghese

Model Checking Finite-Horizon Markov Chains with Probabilistic Inference  (CAV 2021)
       Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd Millstein, Sanjit A. Seshia, Guy Van den Broeck

Logical Abstractions for Noisy Variational Quantum Algorithm Simulation  (ASPLOS 2021, IEEE Micro Top Picks Honorable Mention)
       Yipeng Huang, Steven Holtzen, Todd Millstein, Guy Van den Broeck, Margaret Martonosi

Counterexample-Guided Learning of Monotonic Neural Networks  (NeurIPS 2020)
       Aishwarya Sivaraman, Golnoosh Farnadi, Todd Millstein, Guy Van den Broeck

Scaling Exact Inference for Discrete Probabilistic Programs  (OOPSLA 2020, Distinguished Paper Award)
       Steven Holtzen, Guy Van den Broeck, Todd Millstein

GRoot: Proactive Verification of DNS Configurations  (SIGCOMM 2020, Best Student Paper Award)
       Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd Millstein, George Varghese

Data-Driven Inference of Representation Invariants  (PLDI 2020, Distinguished Paper Award)
       Anders Miltner, Saswat Padhi, Todd Millstein, David Walker

Finding Network Misconfigurations by Automatic Template Inference  (NSDI 2020)
       Siva Kesava Reddy Kakarla, Alan Tang, Ryan Beckett, Karthick Jayaraman, Todd Millstein, Yuval Tamir, George Varghese

Don't Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations (Brief Reflections on Abstractions for Network Programming)  (CCR)
       Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, David Walker

Generating and Sampling Orbits for Lifted Probabilistic Inference  (UAI 2019, Oral Presentation)
       Steven Holtzen, Todd Millstein, Guy Van den Broeck

Overfitting in Synthesis: Theory and Practice  (CAV 2019)
       Saswat Padhi, Todd Millstein, Aditya Nori, Rahul Sharma

Accelerating Sequential Consistency for Java with Speculative Compilation  (PLDI 2019)
       Lun Liu, Todd Millstein, Madanlal Musuvathi

FlashProfile: A Framework for Synthesizing Data Profiles  (OOPSLA 2018)
       Saswat Padhi, Prateek Jain, Daniel Perelman, Oleksandr Polozov, Sumit Gulwani, Todd Millstein

Adding data provenance support to Apache Spark  (VLDB Journal, Special issue on best papers of VLDB 2016)
       Matteo Interlandi, Ari Ekmekji, Kshitij Shah, Muhammad Ali Gulzar, Sai Deep Tetali, Miryung Kim, Todd Millstein, Tyson Condie

Sound Abstraction and Decomposition of Probabilistic Programs  (ICML 2018)
       Steven Holtzen, Guy Van den Broeck, Todd Millstein

A Volatile-by-Default JVM for Server Applications  (OOPSLA 2017)
       Lun Liu, Todd Millstein, Madanlal Musuvathi

Probabilistic Program Abstractions  (UAI 2017)
       Steven Holtzen, Todd Millstein, Guy Van den Broeck

Network Configuration Synthesis with Abstract Topologies  (PLDI 2017)
       Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, David Walker

Efficient Network Reachability Analysis Using a Succinct Control Plane Representation  (OSDI 2016)
       Seyed K. Fayaz, Tushar Sharma, Ari Fogel, Ratul Mahajan, Todd Millstein, Vyas Sekar, George Varghese

Optimizing Interactive Development of Data-Intensive Applications  (SOCC 2016)
       Matteo Interlandi, Sai Deep Tetali, Muhammad Ali Gulzar, Joseph Noor, Tyson Condie, Miryung Kim, Todd Millstein

DRFx: An Understandable, High Performance, and Flexible Memory Model for Concurrent Languages  (TOPLAS)
       Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy

Don't Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations  (SIGCOMM 2016, Best Paper Award)
       Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, David Walker

Technical Perspective: Toward Reliable Programming for Unreliable Hardware  (CACM)
       Todd Millstein

Interactive Debugging for Big Data Analytics  (HotCloud 2016)
       Muhammad Ali Gulzar, Xueyuan Han, Matteo Interlandi, Shaghayegh Mardani, Sai Deep Tetali, Tyson Condie, Todd Millstein, Miryung Kim

Data-Driven Precondition Inference with Learned Features  (PLDI 2016, Winner of the Invariant Synthesis track in both the 2017 and 2018 Syntax Guided Synthesis Competition)
       Saswat Padhi, Rahul Sharma, Todd Millstein

BigDebug: Debugging Primitives for Interactive Big Data Processing in Spark  (ICSE 2016)
       Muhammad Ali Gulzar, Matteo Interlandi, Seunghyun Yoo, Sai Deep Tetali, Tyson Condie, Todd Millstein, Miryung Kim

Titian: Data Provenance Support in Spark  (PVLDB, Selected for The VLDB Journal's special issue on best papers of VLDB 2016)
       Matteo Interlandi, Kshitij Shah, Sai Deep Tetali, Muhammad Ali Gulzar, Seunghyun Yoo, Miryung Kim, Todd Millstein, Tyson Condie

Checks and Balances: Constraint Solving without Surprises in Object-Constraint Programming Languages  (OOPSLA 2015)
       Tim Felgentreff, Todd Millstein, Alan Borning, Robert Hirschfeld

The Silently Shifting Semicolon  (SNAPL 2015)
       Daniel Marino, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, Abhayendra Singh

A General Approach to Network Configuration Analysis  (NSDI 2015)
       Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, Todd Millstein

Analyzing Protocol Implementations for Interoperability  (NSDI 2015)
       Luis Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, Todd Millstein

Call by Meaning  (Onward! 2014)
       Hesam Samimi, Chris Deaton, Yoshiki Ohshima, Alessandro Warth, Todd Millstein

Automatic Atomicity Verification for Clients of Concurrent Data Structures  (CAV 2014)
       Mohsen Lesani, Todd Millstein, Jens Palsberg

MrCrypt: Static Analysis for Secure Cloud Computations  (OOPSLA 2013)
       Sai Deep Tetali, Mohsen Lesani, Rupak Majumdar, Todd Millstein

Declarative Mocking  (ISSTA 2013)
       Hesam Samimi, Rebecca Hicks, Ari Fogel, Todd Millstein

A Safety-First Approach to Memory Models  (IEEE Micro)
       Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi

RERAN: Timing- and Touch-Sensitive Record and Replay for Android  (ICSE 2013)
       Lorenzo Gomez, Iulian Neamtiu, Tanzirul Azim, Todd Millstein

Dr. Android and Mr. Hide: Fine-grained Permissions in Android Applications  (SPSM 2012)
       Jinseong Jeon, Kristopher K. Micinski, Jeffrey A. Vaughan, Ari Fogel, Nikhilesh Reddy, Jeffrey S. Foster, Todd Millstein

Secure Information Flow for Concurrent Programs under Total Store Order  (CSF 2012)
       Jeffrey A. Vaughan, Todd Millstein

End-to-End Sequential Consistency  (ISCA 2012, IEEE Micro Top Pick)
       Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi

Automated Repair of HTML Generation Errors in PHP Applications Using String Constraint Solving  (ICSE 2012)
       Hesam Samimi, Max Schäfer, Shay Artzi, Todd Millstein, Frank Tip, Laurie Hendren

Tool-supported Refactoring for JavaScript  (OOPSLA 2011)
       Asger Felthaus, Todd Millstein, Anders Møller, Max Schäfer, Frank Tip

Finding Protocol Manipulation Attacks  (SIGCOMM 2011)
       Nupur Kothari, Ratul Mahajan, Todd Millstein, Ramesh Govindan, Madanlal Musuvathi

A Case for an SC-Preserving Compiler  (PLDI 2011)
       Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy

Efficient Processor Support for DRFx, a Memory Model with Exceptions  (ASPLOS 2011)
       Abhayendra Singh, Daniel Marino, Satish Narayanasamy, Todd Millstein, Madanlal Musuvathi

Falling Back on Executable Specifications  (ECOOP 2010)
       Hesam Samimi, Ei Darli Aung, Todd Millstein

DRFx: A Simple and Efficient Memory Model for Concurrent Programming Languages  (PLDI 2010)
       Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy

JavaCOP: Declarative Pluggable Types for Java  (TOPLAS)
       Shane Markstrum, Daniel Marino, Matthew Esquivel, Todd Millstein, Chris Andreae, James Noble

Fine-Grained Access Control with Object-Sensitive Roles  (ECOOP 2009)
       Jeffrey Fischer, Daniel Marino, Rupak Majumdar, Todd Millstein

Expressive and Modular Predicate Dispatch for Java  (TOPLAS)
       Todd Millstein, Christopher Frost, Jason Ryder, Alessandro Warth

A Generic Type-and-Effect System  (TLDI 2009)
       Daniel Marino, Todd Millstein

Can You Fool Me? Towards Automatically Checking Protocol Gullibility  (HotNets 2008)
       Milan Stanojevic, Ratul Mahajan, Todd Millstein, Madanlal Musuvathi

An Extensible State Machine Pattern for Interactive Applications  (ECOOP 2008)
       Brian Chin, Todd Millstein

Deriving State Machines from TinyOS Programs using Symbolic Execution  (IPSN 2008, Best Paper Award)
       Nupur Kothari, Todd Millstein, Ramesh Govindan

Packrat Parsers Can Support Left Recursion  (PEPM 2008)
       Alessandro Warth, James R. Douglass, Todd Millstein

Reliable and Efficient Programming Abstractions for Wireless Sensor Networks  (PLDI 2007)
       Nupur Kothari, Ramakrishna Gummadi, Todd Millstein, Ramesh Govindan

Enforcing and Validating User-Defined Programming Disciplines  (PASTE 2007)
       Brian Chin, Daniel Marino, Shane Markstrum, Todd Millstein

Declarative Failure Recovery for Sensor Networks  (AOSD 2007)
       Ramakrishna Gummadi, Nupur Kothari, Todd Millstein, Ramesh Govindan

Tasks: Language Support for Event-driven Programming  (PEPM 2007)
       Jeffrey Fischer, Rupak Majumdar, Todd Millstein

Statically Scoped Object Adaptation with Expanders  (OOPSLA 2006)
       Alessandro Warth, Milan Stanojevic, Todd Millstein

A Framework for Implementing Pluggable Type Systems  (OOPSLA 2006)
       Chris Andreae, James Noble, Shane Markstrum, Todd Millstein

Mechanized Metatheory for User-Defined Type Extensions  (WMM 2006)
       Daniel Marino, Brian Chin, Todd Millstein, Gang Tan, Robert Simmons, David Walker

Responders: Language Support for Interactive Applications  (ECOOP 2006)
       Brian Chin, Todd Millstein

MultiJava: Design Rationale, Compiler Implementation, and Applications  (TOPLAS)
       Curtis Clifton, Todd Millstein, Gary Leavens, Craig Chambers

Inference of User-Defined Type Qualifiers and Qualifier Rules  (ESOP 2006)
       Brian Chin, Shane Markstrum, Todd Millstein, Jens Palsberg

Modularly Typesafe Interface Dispatch in JPred  (FOOL/WOOD 2006)
       Christopher Frost, Todd Millstein

Semantic Type Qualifiers  (PLDI 2005)
       Brian Chin, Shane Markstrum, Todd Millstein

Cobalt: A Language for Writing Provably-Sound Compiler Optimizations  (ENTCS)
       Sorin Lerner, Todd Millstein, Craig Chambers

Polymorphic Predicate Abstraction  (TOPLAS)
       Thomas Ball, Todd Millstein, Sriram Rajamani

Generating Error Traces from Verification-Condition Counterexamples  (SCP)
       Rustan Leino, Todd Millstein, James Saxe

Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules  (POPL 2005)
       Sorin Lerner, Todd Millstein, Erika Rice, Craig Chambers

Bounded Similarity Querying for Time-Series Data  (I&C)
       Dina Goldin, Todd Millstein, Ayferi Kutlu

Practical Predicate Dispatch  (OOPSLA 2004)
       Todd Millstein

Modular Typechecking for Hierarchically Extensible Datatypes and Functions  (TOPLAS)
       Todd Millstein, Colin Bleckner, Craig Chambers

Reconciling Software Extensibility with Modular Program Reasoning  (Ph.D. Dissertation)
       Todd Millstein

Relaxed MultiJava: Balancing Extensibility and Modular Typechecking  (OOPSLA 2003)
       Todd Millstein, Mark Reay, Craig Chambers

Automatically Proving the Correctness of Compiler Optimizations  (PLDI 2003, Best Paper Award)
       Sorin Lerner, Todd Millstein, Craig Chambers

Query Containment for Data Integration Systems  (JCSS)
       Todd Millstein, Alon Halevy, Marc Friedman

Modular Typechecking for Hierarchically Extensible Datatypes and Functions  (ICFP 2002)
       Todd Millstein, Colin Bleckner, Craig Chambers

Modular Statically Typed Multimethods  (I&C)
       Todd Millstein, Craig Chambers

Automatic Predicate Abstraction of C Programs  (PLDI 2001, 2011 Most Influential PLDI Paper Award)
       Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram Rajamani

MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java  (OOPSLA 2000)
       Curtis Clifton, Gary Leavens, Craig Chambers, Todd Millstein

Query Containment for Data Integration Systems  (PODS 2000)
       Todd Millstein, Alon Halevy, Marc Friedman

Navigational Plans for Data Integration  (AAAI 1999)
       Marc Friedman, Alon Halevy, Todd Millstein

Modular Statically Typed Multimethods  (ECOOP 1999)
       Todd Millstein, Craig Chambers

Multiple Dispatch as Dispatch on Tuples  (OOPSLA 1998)
       Gary Leavens, Todd Millstein

Automatic SAT-Compilation of Planning Problems  (IJCAI 1997)
       Michael Ernst, Todd Millstein, Daniel Weld