Constraints over regular and context-free languages are common in the context of string-manipulating programs. Efficient solving of such constraints, often in combination with arithmetic and other theories, has many useful applications in program analysis and testing. We introduce and evaluate a method for symbolically expressing and solving constraints over automata, including subset constraints. Our method uses techniques present in the state-of-the-art SMT solver Z3.

In  LPAR-17

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details

Previous Versions

Margus Veanes, Nikolaj Bjorner, and Leonardo de Moura. Solving Extended Regular Constraints Symbolically, Microsoft Research, December 2009.