Kumar, A., & Manolios, P. (2021). Mathematical Programming Modulo Strings. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 261–270). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_36
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.
CC BY 4.0
