Loris D'Antoni

Loris D'Antoni

Assistant Professor

Dept. of Computer Sciences - Univ. of Wisconsin-Madison
1210 West Dayton Street (Office 6355)
Madison, WI 53706-1685 USA
loris (at) cs (dot) wisc (another dot) edu

My research is about developing cool formal method techniques to solve
cool programming languages problems.

I'm a member of the madPL group and I am looking for talented students/postdocs to work on the following projects. Email your CV if interested.

Foundations of program synthesis

Lay the foundations of program synthesis. Can we predict when and understand why synthesis works? Can we solve synthesis problems with quantitative objectives? What is the relation between synthesis and machine learning? Read more here.

Emulative program repair

Learn good ways to automatically fix errors in programs by looking at how actual programmers fix errors in their programs. Take a look at NoFAQ (command line errors), Refazer (introductory programming assignments), and Revisar (quick Java fixes).

Algorithmic fairness

Use probabilistic program verification to check whether decision-making programs are biased (e.g., discriminate against protected groups) and use synthesis to automaticlly repair biased program to remove bias from them. Take a look at FairSquare and Digits.

Personalized education

Use program verification and program synthesis to build tools that can provide meaningful personalized feedback to students learning core topics in computer sciences. Check out Automata Tutor (automata) and JDial (debugging programs).

Intent-based networking

Allow network operators to verify, design, and repair network configurations by providing high-level intents (i.e., desirable network policies) instead of low-level configurations that are hard to program. Take a look at Genesis and Zeppelin.

Symbolic automata

Design new automaton and transducer models that leverage the power of decidable Boolean theories (e.g., SMT solvers) to reason about strings and tress over complex and infinite alphabets (e.g., UTF16 and integers). Read more here.

Latest news

Apr 19
I will be serving in the program committee for PLATEAU 18.
Apr 2
I will be serving in the program committee for LPAR-22 and I am excited to organize the Midwest Programming Languages Summit 2018.
Mar 31
Two papers accepted at CAV 2018! The Learnability of Symbolic Automata and Syntax Guided Synthesis with Quantitative Syntactic Objectives.
Dec 20
Got the NSF CAREER! ... and Synthesis of Fault-Tolerant Distributed Router Configurations accepted at SIGMETRICS 2018!
July 10
Some press about our fairness project (led by Aws) on UW News and the Wisconsin State Journal.
June 20
FairSquare: Probabilistic Verification of Program Fairness accepted at OOPSLA 2017!
June 2
NoFAQ: Synthesizing Command Repairs from Examples accepted at FSE 2017!
May 5
The long version of Streaming tree transducers will appear in JACM!
May 3
A Symbolic Decision Procedure for Symbolic Alternating Automata accepted at MFPS XXXIII!
Apr 24
Weighted Model Integration with Orthogonal Transformations accepted at IJCAI 2017!
Apr 12
Repairing Decision-Making Programs 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
The next time you need to evaluated your tool on Automata and Temporal Logic you can use the benchmark AutomatArk and contribute with new benchmark for the community to use.
Sep 10
We open-sourced the frontend and backend of Automata Tutor. Feel free to contribute, address issues, and add features. We also made publicly available most of the data we collected.
Apr 15
Qlose: Program Repair with Quantitative Objectives with Roopsha Samanta and Rishab Singh accepted at CAV 2016!
Apr 4
Minimization of symbolic tree automata accepted at LICS 2016!

Selected publications [ full list, DBLP, Google Scholar ]

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 [ 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

Professional activities

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