Loris D’Antoni
The Power of Symbolic Automata
August 09, 2016 at 12:00pm
CSE 305
Abstract
Symbolic Automata allow transitions to carry predicates over rich alphabet theories, such as linear arithmetic, and therefore extend finite automata to operate over infinite alphabets, such as the set of rational numbers. This model can describe sets of lists where elements are drawn from complex theories such as the ones supported by SMT solvers. Symbolic Automata have been used to verify functional programs operating over lists and trees, to prove the correctness of complex implementations of BASE64 and UTF encoders, and they have been integrated with the SMT solver Z3 to support constraints over sequences.
Despite their generality, symbolic automata retain good properties: they are closed under Boolean operations, they can be minimized, and it is decidable to check whether two automata accept the same languages. At the same time, this novel model poses new challenges and opens new opportunities in designing efficient automata decision procedures. In this talk I will present the general features of this formalism and cover two novel decision procedures that exploit the structures of symbolic automata: the first one is a novel algorithm for checking equivalence of two symbolic alternating automata and the second one is an algorithm for minimizing symbolic tree and word automata.
More at: http://pages.cs.wisc.edu/~loris/symbolicautomata.html
Bio
I am an Assistant Professor at the University of Wisconsin, Madison!
My research focuses on combining formal methods and programming languages techniques to make programming simpler, less error-prone, and more efficient. I’m currently working on 1) learning how to repair programs by observing how people react to software errors; and 2) automatically proving quantitative properties of classifiers used in machine learning.