SMT-LIB Sequences and Regular Expressions

Strings are ubiquitous in software. Tools for specification,verification and test-case generation of software rely in various degrees onrepresenting and reasoning about strings. Reasoning about strings isparticularly important in several security critical applications, such asweb sanitizers. Besides a basic representation of strings, applicationsalso use string recognizers and transducers.This paper presents a proposal for an SMT-LIBization of strings and regularexpressions. 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 amongexisting tools for string constraint solving.