SMT-LIB Sequences and Regular Expressions
Nikolaj Bjørner, Vijay S Ganesh, Raphaël Michel, Margus Veanes · EPiC series in computing · 2018
Strings are ubiquitous in software. Tools for specification, verification and test-case generation of software rely in various degrees on representing and reasoning about strings. Reasoning about strings is particularly important in several security critical applications, such as web sanitizers. Besides a basic representation of strings, applications also use string recognizers and transducers. This paper presents a proposal for an SMT-LIBization of strings and regular expressions. It introduces a theory of sequences, generalizing strings, and builds a theory of regular experssions on top of sequences. The logic QF_BVRE is designed to capture a common substrate among existing tools for string constraint solving.