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 Refazer (Python 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

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!