Symbolic Automata Constraint Solving

Margus Veanes, Nikolaj Bjorner, and Leonardo de Moura

Abstract

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.

Details

Publication typeInproceedings
Published inLPAR-17
Volume6397
SeriesLNCS/ARCoSS
PublisherSpringer Verlag

Previous versions

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

> Publications > Symbolic Automata Constraint Solving