I am a final-year Ph.D. student at Penn advised by Rajeev Alur. I am part of the NSF Expeditions in Computer Augmented Program Engineering (ExCAPE) to develop synthesis tools that can partially automate tricky programming tasks.

I am on the academic job market this year (Research Statement, Teaching Statement, CV).

My research focuses on building programming languages and designing techniques that use decision procedures to make programming domain-specific tasks simpler, less error-prone, and more efficient.

During my Ph.D. I designed three programming languages, Bex, Fast, and DReX, that use automata to simplify writing string and tree manipulating programs. I also built AutomataTutor, a tool for teaching finite automata to undergraduate students.

Research Projects

Automata-based Programming Languages: I designed domain-specific languages that use automata techniques to prove program properties and to generate efficient implementations (Bex, Fast, and DReX).
Symbolic Automata: I'm working on combining automata and SMT solvers to reason about strings and tress over complex and infinite alphabets.
AutomataTutor: A tool for teaching finite automata that has already been used at Penn, UIUC, University of Reykjavik, EPFL, and UCSD.

Selected Publications [ full list, DBLP, Google Scholar ]

DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations [ pdf ]
R. Alur, L. D'Antoni, M. Raghothaman,
Approved by the POPL15 artifact evaluation committee!
Program Boosting: Program Synthesis via Crowd-Sourcing [ pdf ]
R. Cochran, L. D'Antoni, B. Livshits, D. Molnar, M. Veanes
Symbolic Visibly Pushdown Automata [ pdf ]
L. D'Antoni, R. Alur
CAV 14
Fast: A Transducer-Based Language for Tree Manipulation [ short pdf, pdf, slides ]
L. D'Antoni, M. Veanes, B. Livshits, D. Molnar,
Fast is live, try it out!
Minimization of Symbolic Automata [ pdf, slides ]
L. D'Antoni, M. Veanes
Regular Functions, Register Cost Automata, and Generalized Min-Cost Problems [ pdf ]
R. Alur, L. D'Antoni, J. V. Deshmukh, M. Raghothaman, Y. Yuan
Automated Grading of DFA Constructions [ pdf, slides ]
R. Alur, L. D'Antoni, S. Gulwani, D. Kini, M. Viswanathan,
AutomataTutor is live, try it out!
Operating System Support For Augmented Reality Applications [ pdf ]
L. D'Antoni, A. Dunn, T. Kohno, B. Livshits, D. Molnar, A. Moshchuk, E. Ofek, F. Roesner, S. Saponas, M. Veanes, and H.J. Wang
HotOS 13
Equivalence of Extended Symbolic Finite Transducers [ pdf, slides ]
L. D'Antoni, M. Veanes,
Selected for the Special Issue of the journal Formal Methods in System Design for CAV 2013!
CAV 13
High-Performance Complex Event Processing over Hierarchical Data [ pdf ]
B. Mozafari, K. Zeng, L. D'Antoni, C. Zaniolo
Static Analysis of String Encoders and Decoders [ pdf, slides ]
L. D'Antoni, M. Veanes
Streaming Tree Transducers [ short pdf, pdf, slides ]
R. Alur, L. D'Antoni


Programming using Automata and Transducers [ link ]
L. D'Antoni, M. Veanes

Professional Activities

CAV 2015: PC Member of the Artifact Evaluation Commitee


Teaching Assistant for CIS 262: Automata, Computability, and Complexity (Fall 2011).
Teaching Assistant for CIS 500: Software foundations (Spring 2012).
I built AutomataTutor, a tool that automatically grades and provides feedback for automata constructions. The tool is being used for teaching automata at Penn, UIUC, University of Reykjavik, and EPFL.
I'm a secondary contributor of the ebook Software foundations, used to teach Coq in many universities.


Sport: volleyball, squash, soccer, hiking., climbing...
Magic: cards, coins, and more.
Cooking and eating what I cook.
Music: piano, saxophone, drums.