My main interests are verification, programming languages, and automata theory. Here are my main projects:
Automata based Programming Languages: my goal is to design domain specific languages
that, using automata and transducers techniques, can perform useful program analysis for non-trivial program tasks and enable
fast execution in performance and securitycritical applications
(see Bex for analysis of string encdoer, and Fast
for analysis and efficient executions of tree manipulating programs).
Symbolic Automata: Classical automata do not handle infinite alphabets
and often do not scale in the presence of ver large alphabets (UTF16 has 2^16 alphabet symbols).
Symbolic Auotmata address this problem by representing the alphabet symbolically using a separate theory. In practice
this is achieved via an integration with an SMT solver. Check this page for more information.
a tool for teaching finite automata that uses formal techniques for grading and feedback generation.
The tool has already been used in real classes at Penn, UIUC, and University of Reykjavik with positive results
and enthusiastic feedback from both students and teachers.
Fast: A Transducer-Based Language for Tree Manipulation
[short pdf, pdf]
L. D'Antoni, M. Veanes, B. Livshits, D. Molnar
35th annual ACM SIGPLAN conference on Programming Language Design and Implementation
Fast is live, try it out!!
Minimization of Symbolic Automata [pdf, slides]
L. D'Antoni, M. Veanes
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014
Regular Functions, Register Cost Automata, and Generalized Min-Cost Problems [short pdf, pdf]
R. Alur, L. D'Antoni, J. V. Deshmukh, M. Ragothaman, and Y. Yuan
28th ACM/IEEE Symposium on Logic in Computer Science, 2013
Automated Grading of DFA Constructions [pdf, slides]
R. Alur, L. D'Antoni, S. Gulwani, D. Kini, and M. Viswanathan
23th International Joint Conference on Artificial Intelligence, 2013
AutomataTutor is live, try it out!!
Equivalence of Extended Symbolic Finite Transducers [short pdf, pdf, slides]
L. D'Antoni, and M. Veanes
in Proceedings of
25th International Conference on Computer-Aided Verification, 2013
Bex is live, try it out!!
High-Performance Complex Event Processing over Hierarchical Data
B. Mozafari, K. Zeng, L. D'Antoni, and C. Zaniolo
In ACM TODS's Special Issue on "Best of SIGMOD", Dec, 2013
Static Analysis of String Encoders and Decoders [pdf, slides]
L. D'Antoni, and M. Veanes
14th International Conference on Verification, Model Checking, and Abstract Interpretation, 2013
Streaming Tree Transducers [short pdf, pdf, slides]
R. Alur, and L. D'Antoni
39th International Colloquium on Automata, Languages, and Programming, 2012
Fall 2011: Teaching Assistant
for CIS 262: Automata, Computability, and Complexity.
Spring 2012: Teaching Assistant
for CIS 500: Software foundations.
2013: Summer Intership at Microsoft Research supervised by Margus Veanes.
2012: Summer Intership at Microsoft Research supervised by Margus Veanes.
Research fellowship BIOBITS at
Universita' degli studi di Torino.
Music: piano, saxophone, drums;
Sport: squash, soccer, volleyball;
Magic: cards, coins, and more;
Cooking and Japanese Animation