Margus Veanes, Nikolaj Bjorner, and Leonardo de Moura
Constraints over regular expressions are common in programming languages, often in combination with other constraints involving strings. Efficient solving of such constraints has many useful applications in program analysis and testing. We introduce a method for symbolically expressing and analyzing regular constraints using state of the art SMT solving techniques. The method is implemented using the SMT solver Z3 and is evaluated over a collection of benchmarks.
© 2009 Microsoft Corporation. All rights reserved.
Margus Veanes, Nikolaj Bjorner, and Leonardo de Moura. Symbolic Automata Constraint Solving, Springer Verlag, October 2010.