Share on Facebook Tweet on Twitter Share on LinkedIn Share by email

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.

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.