Mathematical Programming Modulo Strings

We introduce TranSeq, a non-deterministic, branching transition system for deciding the satisfiability of conjunctions of string equations. TranSeq is an extension of the Mathematical Programming Modulo Theories (MPMT) constraint solving framework and is designed to enable useful and computationally efficient inferences that reduce the search space, that encode certain string constraints and theory lemmas as integer linear constraints and that otherwise split problems into simpler cases, via branching. We have implemented a prototype, SeqSolve, in ACL2s, which uses Z3 as a back-end solver. String solvers have numerous applications, including in security, software engineering, programming languages and verification. We evaluated SeqSolve by comparing it with existing tools on a set of benchmark problems and our experimental results show that SeqSolve is both practical and efficient.22612701