Mathematical Programming Modulo Strings

---

Ankit Kuman and Panagiotis Manolios.
FMCAD, 2021

Abstract

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 engi- neering, 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.

PDF (412K)