Department of Information Technology

Strings and Automata Modulo Theories


Margus Veanes, Microsoft Research Redmond

Date and Time

Friday, August 14th, 2015 at 14:15.


Polacksbacken, room 1245


Analysis of string manipulating programs is relevant in many different domains. In real applications, characters in strings often range over Unicode and are usually treated as bit-vectors. In that sense, the theory of strings is really parametric in the theory of characters. This poses a unique challenge in integrating it as a theory into existing SMT solvers. Rather than integrating the theory of strings into an SMT solver, the focus of this talk is to illustrate how one can integrate an SMT solver into a domain specific tool for reasoning about strings. We focus on domain specific languages and tasks that admit automata or transducer based formulations, such as regexes, and specialized languages for string sanitizers, string encoders, and string decoders. Many analysis problems over strings that can be formulated through automata or transducer based algorithms become scalable through extensions based on using an SMT solver. Such algorithm extensions also pose new challenges in the automata community.

Updated  2015-08-13 16:55:00 by Philipp Rümmer.