PLSE Seminar Series - The Power of Symbolic Automata

Explore the power and applications of Symbolic Automata in this seminar talk by Loris D'Antoni. Delve into the world of automata that operate over infinite alphabets, such as rational numbers, using predicates over rich alphabet theories like linear arithmetic. Discover how this model extends finite automata and its applications in verifying functional programs, proving correctness of complex implementations, and integration with SMT solvers. Learn about the unique properties of Symbolic Automata, including closure under Boolean operations, minimization capabilities, and decidability of language equivalence. Gain insights into novel decision procedures that exploit the structures of symbolic automata, including an algorithm for checking equivalence of symbolic alternating automata and a method for minimizing symbolic tree and word automata. Presented by Assistant Professor Loris D'Antoni from the University of Wisconsin, Madison, whose research focuses on combining formal methods and programming languages techniques to simplify programming, reduce errors, and improve efficiency.