Loris D'Antoni

Loris D'Antoni

Jacobs Faculty Scholar &
Associate Professor

Computer Science and Engineering - UCSD (Office 3214)
3235 Voigt Dr, La Jolla, CA 92093 USA
[email protected]

My research is about helping people write trustworthy software.

I'm a professor in the Programming Systems Group and a visiting academic at AWS. Before joining UCSD, I co-founded the group at UW-Madison.

Specification-aligned LLMs

Formal techniques for constraining the output of large language models of code. Just started, but take a look at my prior work on trustworthy ML like Antidote and A3T.

Semantics-guided synthesis

A framework for specifying and solving arbitrary synthesis problems. Paper and website.

Selected publications [ DBLP, Google Scholar ]

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

2025
LLM4Code, VMCAI, OOPSLA, PLDI
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