Automata - Microsoft Research

Automata

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

Rex is a command line tool that generates matching strings for .NET regexes.
Bek is a tool for sanitizing web services for cross-site scripting attacks.
Pex is a tool for generating unit tests for .NET code.

Downloads

Microsoft Research Automata Tool Kit
27 October 2011 · Version: 1.0.0.0

Online Demos

Rex is showcased using a duel mode, where the user is tasked with guessing a secret regular expression.

Bek is showcased with sample sanitizers.

People

Margus Veanes

Publications

Margus Veanes, Minimization of Symbolic Automata, no. MSR-TR-2013-48, April 2013
Margus Veanes and Nikolaj Bjorner, Symbolic Automata: The Toolkit, in TACAS'12, Springer Verlag, March 2012

Share