Todd Millstein
where else to find them
no profile links on file
what they talk about
all 8 in the filters
where they keep going back
- OOPSLA3 editions2020–2025
all 8 in the filters
on a stage with
all 19 in the filters
who talks about the same things
- Guy Van den Broeck8 talks
- Steven Holtzen12 talks
- Poorva Garg3 talks
- Harrison Goldstein10 talks
- Benjamin C. Pierce17 talks
- Mathieu Huot11 talks
| title | conference | date |
|---|---|---|
| Eywa: Automating Model-Based Testing using LLMs | NSDI '26 | 2026-05-04 |
Eywa uses LLMs to synthesize modular, executable protocol models (converted to code and composed via dependency graphs) and then drives KLEE-style symbolic… | ||
| Tuning Random Generators: Property-Based Testing as Probabilistic Programming | OOPSLA 2025 | 2025-10-16 |
Generators become probabilistic programs with symbolic weights and are tuned by computing a symbolic distribution, compiling it into compressed BDD-based… | ||
| Synthesizing Implication Lemmas for Interactive Theorem Proving | OOPSLA 2025 | 2025-10-16 |
Implements a Rocq tactic called dilemma that synthesizes implication lemmas of the form P1 ∧ … ∧ Pn ⇒ Q by data-driven invariant inference over sample… | ||
| Welcome | JENSFEST 2024 | 2024-10-22 |
A short welcome recounts concrete ways Jens shapes careers: three roles — mentor, citizen, explorer — with specifics: coauthored the presenter's first grant… | ||
| Bit Blasting Probabilistic Programs | PLDI 2024 | 2024-06-24 |
Presents a new discretization called bit blasting that encodes continuous variables as Boolean bits so a domain of 2^b points becomes a discrete program over… | ||
| MESSI: Behavioral Testing of BGP Implementations | 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24) | 2024-04-16 |
MESSI is a model-based tester that symbolically generates joint configuration–state–route triples to exercise BGP behavior, producing about 150K tests and… | ||
| Bit-Blasting Probabilistic Programs | LAFI 2023 | 2023-01-15 |
HyBit converts continuous variables into a discrete bitblasted representation by encoding each real as independent Bernoulli bits, then runs exact inference… | ||
| Data-Driven Lemma Synthesis for Interactive Proofs | OOPSLA 2022 | 2022-12-05 |
A tool called lfind as a Coq tactic reduces lemma synthesis to a data-driven program synthesis problem: it generalizes a stuck goal, generates input/output… | ||
| SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers | 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22) | 2022-04-04 |
SCALE uses an executable RFC model to jointly generate zone files and queries and Ferret runs those tests against real servers. The pipeline uses the Zen… | ||
| Scaling Exact Inference for Discrete Probabilistic Programs | OOPSLA 2020 | 2020-11-15 |
Introduces Dice as a discrete PPL that compiles programs to binary decision diagrams and performs inference by weighted model counting, reusing compiled… | ||
| Finding Network Misconfigurations by Automatic Template Inference | NSDI 2020 | 2020-02-25 |
Automatic inference groups similar router config snippets into parameterized templates and flags small groups as outliers; implemented in the tool SelfStarter… | ||
| nothing matches | ||