Loris D'Antoni

Loris D'Antoni

Department of Computer and Information Science
Ph.D. student
University of Pennsylvania
Levine 565
3330 Walnut Street, Philadelphia, PA 19104-6389
lorisdan (at) seas (dot) upenn (another dot) edu

I am a fifth year Ph.D student, advised by Rajeev Alur.
I previously studied at the Universita' degli studi di Torino where I got my master's degree in computer science.

CV | LinkedIn | Quora


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.
  • AutomataTutor: 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.

Selected Publications (Full List of Publications, DBLP, Google Scholar)

  • Symbolic Visibly Pushdown Automata [ pdf ]
    L. D'Antoni, R. Alur, CAV 2014
  • Fast: A Transducer-Based Language for Tree Manipulation [ short pdf, pdf, slides ]
    L. D'Antoni, M. Veanes, B. Livshits, D. Molnar, PLDI 2014
    Fast is live, try it out!!
  • Minimization of Symbolic Automata [ pdf, slides ]
    L. D'Antoni, M. Veanes, POPL 2014
  • Regular Functions, Register Cost Automata, and Generalized Min-Cost Problems [ short pdf, pdf ]
    R. Alur, L. D'Antoni, J. V. Deshmukh, M. Ragothaman, Y. Yuan , LICS 2013
  • Automated Grading of DFA Constructions [ pdf, slides ]
    R. Alur, L. D'Antoni, S. Gulwani, D. Kini, M. Viswanathan, IJCAI 2013
    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 2013
  • Equivalence of Extended Symbolic Finite Transducers [ short pdf, pdf, slides ]
    L. D'Antoni, M. Veanes, CAV 2013
    Selected for the Special Issue of the journal Formal Methods in System Design for CAV 2013!!
  • High-Performance Complex Event Processing over Hierarchical Data [ pdf ]
    B. Mozafari, K. Zeng, L. D'Antoni, C. Zaniolo, ACM TODS 2013
  • Static Analysis of String Encoders and Decoders [ pdf, slides ]
    L. D'Antoni, M. Veanes, VMCAI 2013
  • Streaming Tree Transducers [ short pdf, pdf, slides ]
    R. Alur, L. D'Antoni, ICALP 2012


  • Fall 2011: teaching Assistant for CIS 262: Automata, Computability, and Complexity.
  • Together with other researchers at Penn, Berkeley, UIUC, and MSR I built AutomataTutor, a tool that automatically grades and provide feedback for automata constructions. The tool is being used for teaching automata in undergraduate courses at Penn, UIUC, University of Reykjavik, and EPFL.
  • Spring 2012: teaching Assistant for CIS 500: Software foundations
  • I'm a secondary contributor of the ebook Software foundations that is being used to teach Coq and programming languages in many universities around the world.

Selected Press

  • Programming language research for K-16 education (Part II) [ article ]
    S. Chaudhuri, The Programming Language Enthusiast


  • EECS 294-98: Formal Methods for Engineering Education [ course link ]
    S. Seshia talks about AutomataTutor and our IJCAI paper in his course on MOOCs.
  • Industry Internships: Where Theory meets practice [ slides ]
    T. Ball explains to the students attending PLMW14 what I did during my internship at MSR in summer 13.
  • Insane in the IFRAME: The case for client-side HTML sanitization [ slides ]
    D. Ross presents JSanity at OWASP AppSec EU 2013, and shows how the preliminary version of the tool was part of the Fast project.
  • MFoCS Research seminar 2014 at Radboud Nijmegen University [ course link ]
    A. Silva teaches symbolic automata and our new minimization algorithm.


Music: piano, saxophone, drums;
Sport: squash, soccer, volleyball;
Magic: cards, coins, and more;
Cooking and Japanese Animation