I am an Assistant Professor at the University of Wisconsin, Madison.
I am looking for talented graduate students and postdocs. Send me an email with your CV if you are interested.

My research focuses on combining formal methods and programming languages techniques to make programming simpler, less error-prone, and more efficient. Lately, I am particularly interested in program repair, synthesis for networking, synthesis for personalized education, symbolic automata, and algorithmic fairness.

What's new?

Apr 24
Weighted Model Integration with Orthogonal Transformations accepted at IJCAI 2017!
Apr 12
Program Repair under Uncertainty accepted at CAV 2017, where I was also invited to give a tutorial on The power of symbolic automata and transducers!
Feb 13
Received the Google Faculty Research Award! Moreover, Automatic Program Inversion using Symbolic Transducers and Control-Flow Recovery from Partial Failure Reports accepted at PLDI 2017!
Dec 22
Learning Symbolic Automata accepted at TACAS 2017 and nominated for best paper award! Forward Bisimulations for Nondeterministic Symbolic Finite Automata also accepted at TACAS 2017!
Dec 21
The work on Refazer produced one paper at L@S and one at ICSE17.
Oct 3
Monadic second-order logic on finite sequences and Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks accepted at POPL 2017!
Sep 20
Next time you need to evaluate your Automata and Temporal Logic tools use the benchmarks in AutomatArk! New benchmarks are always welcome!

Research topics

Program synthesis
Develop the theoretical foundations of program synthesis and learn how to apply it to real world problems. Take a look at Genesis.
Algorithmic fairness
Design new probabilistic verification and inference techniques and use them to verify whether decision-making program discriminate against protected groups. Take a look at this paper.
Personalized education
Use program verification and program synthesis to build tools that can provide meaningful feedback to students learning core topics in computer sciences. Check out Automata Tutor and Refazer.
Symbolic Automata
Combine automata and SMT solvers to reason about strings and tress over complex and infinite alphabets. Read more here.

Selected publications [ full list, DBLP, Google Scholar ]

IJCAI 17
Weighted Model Integration with Orthogonal Transformations
D. Merrell, A. Albarghouthi, L. D'Antoni
CAV 17
Program Repair under Uncertainty
S. Drews, A. Albarghouthi, L. D'Antoni
PLDI 17
Automatic Program Inversion using Symbolic Transducers [ pdf ]
Q. Hu and 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 and L. D'Antoni
TACAS 17
Forward Bisimulations for Nondeterministic Symbolic Finite Automata [ pdf ]
L. D'Antoni and 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 and 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 [ link ]
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
ICALP 12
Streaming Tree Transducers [ short pdf, pdf, slides ]
R. Alur, L. D'Antoni

Teaching and advising

PhD Students
Samuel Drews (co-advised with Aws Albarghouthi), Heping Hu, David Merrell (co-advised with Aws Albarghouthi), Kausik Subramanian (co-advised with Aditya Akella)
Undergraduates
Isaac Evavold, Fang Wang, Sang Yun Park, Chris Gottsacker, Salil Dureja
CS536
Intro to PLs and Compilers (S16, F16)
CS703
Program verification and synthesis (F15)

Professional activities

PC
CAV-AEC15, PLOOC15, CAV16, PLDI16, ICALP16, POPL18
ERC
POPL16, POPL17
Organizer
PLMW@POPL17

Hobbies

Sport, Magic, Cooking, Music.