Strings and Automata Modulo Theories
Speaker
Margus Veanes
, Microsoft Research Redmond
Date and Time
Friday, August 14th, 2015 at 14:15.
Location
Polacksbacken, room 1245
Abstract
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.