Symbolic Automata: The Toolkit

The symbolic automata toolkit lifts classical automata analysis to work modulo rich alphabet theories. It uses the power of state-of-the-art constraint solvers for automata analysis that is both expressive and effifficient, even for automata over large finite alphabets. The toolkit supports analysis of finite symbolic automata and transducers over strings. It also handles transducers with registers. Constraint solving is used when composing and minimizing automata, and a much deeper and powerful integration is also obtained by internalizing automata as theories. The toolkit, freely available from Microsoft Research, has recently been used in the context of web security for analysis of potentially malicious data over Unicode characters.

symAutTACAS12.pdf
PDF file

In  TACAS'12

Publisher  Springer Verlag

Details

TypeInproceedings
SeriesLNCS
> Publications > Symbolic Automata: The Toolkit