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 efficient, 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.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Brucker, Achim D.; Wolff, Burkhart: Monadic sequence testing and explicit test-refinements (2016)
- Courcelle, Bruno; Durand, Irène: Computations by fly-automata beyond monadic second-order logic (2016)
- Yu, Fang; Alkhalaf, Muath; Bultan, Tevfik; Ibarra, Oscar H.: Automata-based symbolic string analysis for vulnerability detection (2014)
- Veanes, Margus; Bjørner, Nikolaj: Symbolic automata: the toolkit (2012)