Automata is a .NET tool kit that provides facilities for manipulating and analyzing regular expressions, symbolic finite automata, and symbolic finite transducers. It supports automata and transducers where input and output alphabets can be fully symbolic. Constraints over the alphabets can be analyzed using Satisfiability Modulo Theory (SMT) solvers. The tool kit provides a particular extension that uses the Microsoft SMT solver Z3.
The main library provided by the project is Microsoft.Automata.dll.
The library can be used as an extension point of Z3 by using the assembly Microsoft.Automata.Z3.dll.
Tools using the Microsoft Research Automata Toolkit
New: In the process of becoming an Open Source Project on GitHub
- Loris D’Antoni and Margus Veanes, Extended symbolic finite automata and transducers, in Formal Methods in System Design , Springer, July 2015.
- Margus Veanes, Todd Mytkowicz, David Molnar, and Benjamin Livshits, Data-Parallel String-Manipulating Programs, in POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM – Association for Computing Machinery, January 2015.
- Loris D'Antoni and Margus Veanes, Minimization of Symbolic Automata, in POPL'14, ACM, January 2014.
- Margus Veanes, Applications of Symbolic Finite Automata, in CIAA'13, Springer, July 2013.
- Margus Veanes and Nikolaj Bjorner, Symbolic Automata: The Toolkit, in TACAS'12, Springer Verlag, March 2012.