Loris D'Antoni

Specification-aligned LLMs

Techniques for making large language models generate code that is guaranteed to satisfy formal specifications. See ChopChop and CARS.

Synthesizing Personalized Compilers

Using synthesis to automatically construct compiler components that adapt to a developer's codebase, invariants, and optimization goals. Check out NiceToMeetYou and Germinator.

Selected publications [ DBLP, Google Scholar ]

ArXiV

Bootstrapping Fuzzers for Compilers of Low-Resource Language Dialects Using Language Models [ pdf ]
S. Vaidya, M. Bohme, L. D'Antoni

POPL 27

A Fistful of Abstract Values: Synthesizing the Transformers Compilers Actually Need [ pdf ]
D. Kennedy, X. Peng, Y. Fan, J. Regehr, L. D'Antoni, B. Greenman

NeurIPS 26

Language-based Agent Control [ pdf ]
T. Zhou, L. D'Antoni, N. Polikarpova

OOPSLA 26

Incremental Program Synthesis from Event Logs [ pdf ]
J. Kim, V. Nicolet, J. Dodds, and L. D'Antoni

COLM 26

The Format Tax [ pdf ]
I. Lee, L. D'Antoni, T. Berg Kirkpatrick

ICML 26

Constrained Adaptive Rejection Sampling [ pdf ]
P. Parys, S. Vaidya, T. Berg-Kirkpatrick, L. D'Antoni

ICML 26

Continuous Diffusion Models Can Obey Formal Syntax [ pdf ]
J. Kim, T. Berg-Kirkpatrick, L. D'Antoni

POPL 26

Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers [ pdf ]
X. Peng*, D. Kennedy*, Y. Fan, B. Greenman, J. Regehr, L. D'Antoni

POPL 26

ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models [ pdf ]
S. Nagy*, T. Zhou*, N. Polikarpova, L. D'Antoni

NeurIPS 26

Constrained Sampling for Language Models Should Be Easy: An MCMC Perspective [ pdf ]
E. Anaya Gonzalez*, S. Vaidya*, K. Park, T. Berg-Kirkpatrick, L. D'Antoni

ICML 25

Flexible and Efficient Grammar-Constrained Decoding [ pdf ]
K. Park, T. Zhou, L. D'Antoni

PLDI 25

Verifying Solutions to Semantics-Guided Synthesis Problems [ pdf ]
C. Murphy, K. Johnson, T. Reps, L. D'Antoni

OOPSLA 25

Loud: Synthesizing Strongest and Weakest Specifications [ pdf ]
K. Park, X. Peng, L. D'Antoni

OOPSLA 25

Semantics of Sets of Programs [ pdf ]
J. Kim, S. Nagy, T. Reps, L. D'Antoni

CHI 25

Perceptions of the Fairness Impacts of Multiplicity in Machine Learning [ pdf ]
A. Meyer, Y. Kim, A. Albarghouthi, L. D'Antoni

NeurIPS 24

Grammar-Aligned Decoding [ pdf ]
K. Park, J. Wang, T. Berg-Kirkpatrick, N. Polikarpova, L. D'Antoni

FMCAD 24

Projective Model Counting for IP Addresses in Access Control Policies [ pdf ]
A. Gacek, A. Goel, D. Jovanovic, D. Peebles, N. Rungta, Y. Sharoda

OOPSLA 24

Automatically Reducing Privilege for Access Control Policies [ pdf ]
L. D'Antoni, S. Ding, A. Goel, M. Ramesh, N. Rungta, C. Sung

OOPSLA 24

Synthesizing Formal Semantics from Executable Interpreters [ pdf ]
J. Liu, C. Murphy, A. Grover, K. Johnson, T. Reps, L. D'Antoni

OOPSLA 24

Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics [ pdf ]
K. Johnson, R. Krishnan, T. Reps, L. D'Antoni

OOPSLA 24

Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of Programs [ pdf ]
S. Nagy, J. Kim, T. Reps, L. D'Antoni

CAV 24

The SemGuS Toolkit [ pdf ]
K. Johnson, A. Reynolds, T. Reps, L. D'Antoni

FMCAD 23

Modular System Synthesis [ pdf ]
K. Park, K. Johnson, L. D'Antoni, T. Reps

OOPSLA 23

Synthesizing Specifications [ pdf ]
K. Park, L. D'Antoni, T. Reps

FAccT 23

The Dataset Multiplicity Problem: How Unreliable Data Impacts Predictions [ pdf ]
A. Meyer, A. Albarghouthi, L. D'Antoni

POPL 23

Unrealizability Logic [ pdf ]
J. Kim, L. D'Antoni, T. Reps

ICDCN 23

Learned Load Balancing [ pdf ]
B. Chen, K. Subramanian, L. D'Antoni, A. Akella Best Paper Award

NeurIPS 22

BagFlip: A Certified Defense against Data Poisoning [ pdf ]
Y. Zhang, A. Albarghouthi, L. D'Antoni

FMCAD 22

Synthesizing Transducers from Complex Specifications [ pdf ]
A. Grover, R. Ehlers, L. D'Antoni

OOPSLA 22

Synthesizing Abstract Transformers [ pdf ]
P. Kalita, S. Muduli, L. D'Antoni, T. Reps, S. Roy

TOPLAS

Solving Program Sketches with Large Integer Values [ pdf ]
Q. Hu, R. Singh, L. D'Antoni

PLDI 22

P4BID: Information Flow Control in P4 [ pdf ]
K. Grewal, L. D'Antoni, J. Hsu

NeurIPS 21

Certifying Robustness to Programmable Data Bias in Decision Trees [ pdf ]
A. P. Meyer, A. Albarghouthi, L. D'Antoni

EMNLP 21

Certified Robustness to Programmable Transformations in LSTMs [ pdf ]
Y. Zhang, A. Albarghouthi, L. D'Antoni Selected for Oral Presentation

SBES 21

Learning Quick Fixes from Code Repositories [ pdf ]
R. Rolim, G. Soares, R. Gheyi, T. Barik, L. D'Antoni Distinguished Paper Award

SOSR 21

D2R: Dataplane-Only Policy-Compliant Routing Under Failures [ pdf ]
K. Subramanian, A. Abhashkumar, L. D'Antoni, A. Akella

SIGCOMM 21

Prognosis: Black-Box Analysis of Network Protocol Implementations [ pdf ]
T. Ferreira, H. Brewton, L. D'Antoni, A. Silva

CACM

Automata Modulo Theories [ pdf ]
L. D'Antoni, M. Veanes

CAV 21

Programmable Program Synthesis [ pdf ]
J. Kim, Q. Hu, L. D'Antoni, T. Reps, Invited Keynote

CAV 21

Synthesis with Asymptotic Resource Bounds [ pdf ]
Q. Hu, J. Cyphert, L. D'Antoni, T. Reps

POPL 21

Semantics-guided Synthesis [ pdf ]
J. Kim, Q. Hu, L. D'Antoni, T. Reps

ICML 20

Robustness to Programmable String Transformations via Augmented Abstract Training [ pdf ]
Y. Zhang, A. Albarghouthi, L. D'Antoni

CAV 20

Automata Tutor v3 [ pdf ]
L. D'Antoni, M. Helfrich, J. Kretinsky, E. Ramneantu, M. Weininger

PLDI 20

Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems [ pdf ]
Q. Hu, J. Cyphert, L. D'Antoni, T. Reps

PLDI 20

Proving Data-Poisoning Robustness in Decision Trees [ pdf ]
S. Drews, A. Albarghouthi, L. D'Antoni SIGPLAN Research Highlight

PLDI 20

Detecting Network Load Violations for Distributed Control Planes [ pdf ]
K. Subramanian, A. Abhashkumar, L. D'Antoni, A. Akella

ESOP 20

Solving Program Sketches with Large Integer Values [ pdf ]
R. Pan, Q. Hu, R. Singh, L. D'Antoni Selected for special issue of TOPLAS
Nominated for EAPLS Award for the best ETAPS paper on PL and systems

OOPSLA 19

Automatic Repair of Regular Expressions [ pdf ]
R. Pan, Q. Hu, G. Xu, L. D'Antoni

SAS 19

Direct Manipulation for Imperative Programs [ pdf ]
Q. Hu, R.Samanta, R. Singh, L. D'Antoni

CAV 19

Efficient Synthesis with Probabilistic Constraints [ pdf ]
S. Drews, A. Albarghouthi, L. D'Antoni

CAV 19

Symbolic Register Automata [ pdf ]
L. D'Antoni, T. Ferreira, M. Sammartino, A. Silva

CAV 19

Proving Unrealizability for Syntax-Guided Synthesis [ pdf ]
Q. Hu, J. Breck, J. Cyphert, L. D'Antoni, T. Reps

CAV 18

Syntax Guided Synthesis with Quantitative Syntactic Objectives [ pdf ]
Q. Hu, L. D'Antoni

CAV 18

The Learnability of Symbolic Automata [ pdf ]
G. Argyros, L. D'Antoni

SIGMETRICS 18

Synthesis of Fault-Tolerant Distributed Router Configurations [ pdf ]
K. Subramanian, L. D'Antoni, A. Akella

OOPSLA 17

FairSquare: Probabilistic Verification of Program Fairness [ pdf ]
A. Albarghouthi, L. D'Antoni, S. Drews, A. Nori

FSE 17

NoFAQ: Synthesizing Command Repairs from Examples [ pdf ]
L. D'Antoni, R. Singh, M. Vaughn

VL/HCC 17

TraceDiff: Debugging Unexpected Code Behavior Using Trace Divergence [ pdf ]
R. Suzuki, G Soares, A. Head, E. Glassman, R. Reis, M. Mongiovi, L. D'Antoni, B. Hartmann

JACM

Streaming Tree Transducers [ ICALP pdf, pdf ]
R. Alur, L. D'Antoni

MFPS XXXIII

A Symbolic Decision Procedure for Symbolic Alternating Finite Automata [ pdf ]
L. D'Antoni, Z. Kincaid, F. Wang

IJCAI 17

Weighted Model Integration with Orthogonal Transformations [ pdf ]
D. Merrell, A. Albarghouthi, L. D'Antoni

CAV 17

Repairing Decision-Making Programs under Uncertainty [ pdf ]
S. Drews, A. Albarghouthi, L. D'Antoni

CAV 17

The Power of Symbolic Automata and Transducers [ pdf ]
L. D'Antoni, M. Veanes, Invited Tutorial

PLDI 17

Automatic Program Inversion using Symbolic Transducers [ pdf ]
Q. Hu, L. D'Antoni

PLDI 17

Control-Flow Recovery from Partial Failure Reports [ pdf ]
P. Ohmann, A. Brooks, L. D'Antoni, B. Liblit

TACAS 17

Learning Symbolic Automata [ pdf ]
S. Drews, L. D'Antoni Nominated for best paper award.

TACAS 17

Forward Bisimulations for Nondeterministic Symbolic Finite Automata [ pdf ]
L. D'Antoni, M. Veanes

L@S 17

Writing Reusable Code Feedback at Scale with Mixed-Initiative Program Synthesis [ pdf ]
A. Head, E. Glassman, G. Soares, R. Suzuki, L. Figueredo, L. D'Antoni, B. Hartmann

ICSE 17

Learning Syntactic Program Transformations from Examples [ pdf ]
R. Rolim, G. Soares, L. D'Antoni, O. Polozov, S. Gulwani, R. Gheyi, R. Suzuki, B. Hartmann

POPL 17

Monadic second-order logic on finite sequences [ pdf ]
L. D'Antoni, M. Veanes

POPL 17

Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks [ pdf ]
A. Akella, L. D'Antoni, K. Subramanian

FATML 16

Fairness as a Program Property [ pdf ]
A. Albarghouthi, L. D'Antoni, S. Drews, A. Nori

MICRO-49

HARE: Hardware acceleration for regular expressions [ pdf ]
V. Gogte, A. Kolli, M. Cafarella, L. D'Antoni, T. Wenisch

CAV 16

Qlose: Program Repair with Quantitative Objectives [ pdf ]
L. D'Antoni, R. Samanta, R. Singh

LICS 16

Minimization of Symbolic Tree Automata [ pdf ]
L. D'Antoni, M. Veanes

FMSD 15

Extended Symbolic Finite Automata and Transducers [ pdf ]
L. D'Antoni, M. Veanes

TOPLAS 15

Fast: A Transducer-Based Language for Tree Manipulation (extended version) [ link ]
L. D'Antoni, M. Veanes, B. Livshits, D. Molnar

TOCHI 15

How Can Automatic Feedback Help Students Construct Automata? [ pdf ]
L. D'Antoni, D. Kini, R. Alur, S. Gulwani, M. Viswanathan, B. Hartmann

POPL 15

DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations [ pdf, DReX ]
R. Alur, L. D'Antoni, M. Raghothaman

POPL 15

Program Boosting: Program Synthesis via Crowd-Sourcing [ pdf, slides ]
R. Cochran, L. D'Antoni, B. Livshits, D. Molnar, M. Veanes

CAV 14

Symbolic Visibly Pushdown Automata [ pdf ]
L. D'Antoni, R. Alur

PLDI 14

Fast: A Transducer-Based Language for Tree Manipulation [ pdf, slides, Fast ]
L. D'Antoni, M. Veanes, B. Livshits, D. Molnar

POPL 14

Minimization of Symbolic Automata [ pdf, slides ]
L. D'Antoni, M. Veanes

CAV 13

Equivalence of Extended Symbolic Finite Transducers [ pdf, slides ]
L. D'Antoni, M. Veanes

IJCAI 13

Automated Grading of DFA Constructions [ pdf, slides, Automata Tutor ]
R. Alur, L. D'Antoni, S. Gulwani, D. Kini, M. Viswanathan

LICS 13

Regular Functions, Register Cost Automata, and Generalized Min-Cost Problems [ pdf ]
R. Alur, L. D'Antoni, J. V. Deshmukh, M. Raghothaman, Y. Yuan

VMCAI 13

Static Analysis of String Encoders and Decoders [ pdf, slides ]
L. D'Antoni, M. Veanes

Professional activities

2027

POPL

2026

CAV, TOPLAS (Associate Editor), Reynolds Dissertation Award, SIGPLAN Highlights, SoCalPLS

2025

LLM4Code, VMCAI, OOPSLA, PLDI, ICLR, Reynolds Dissertation Award, SIGPLAN Highlights, SoCalPLS (Chair)

2024

ASPLOS, CAV, ESOP

2023

POPL, PLDI

2022

Sabbatical

2021

POPL, PLDI

2020

APR, NETYS

2019

VMW@CAV, ATVA

2018

POPL, PLDI ERC, CAV, LPAR-22, PLATEAU, Midwest PL Summit

2017

POPL ERC, PLMW@POPL

2016

CAV, PLDI, POPL ERC, ICALP

2015

CAV-AEC, PLOOC