Tutorial:
Symbolic Automata
by Margus Veanes
Abstract
Automata is a .NET tool kit that provides facilities for manipulating and analyzing regular expressions, symbolic finite automata and transducers. It supports automata and transducer algorithms where input and output alphabets can be fully symbolic and it scales for large alphabets, such as Unicode. Constraints over the alphabets can also be analyzed using the SMT solver Z3 as a plugin.
The tutorial will focus on the use of the library as a backend in other tools. It will do so by illustrating a couple of key scenarios: 1) analysis of .NET regexes and how this may benefit various concrete testing scenarios, 2) use of the library for efficient manipulation of automata, including input/output automata (or transducers).
