Improved Integration of String Solvers in SPF

To reason about string manipulating Java programs Symbolic Pathfinder (SPF) employs string constraint solvers. Currently, SPF integrates a limited set of dated string constraint solvers. Since string constraint solvers constantly evolve, there is a continuing need to integrate them with SPF. Adding a new string constraint solver into SPF involves augmentation to the existing SPF code. An in-depth understanding of the SPF solver interface is necessary to accomplish this integration. These obstacles lead to a lack of support for state-of-the-art string constraint solvers in SPF. This proposal outlines changes to SPF that would allow integration of Satisfiability Modulo Theories Library (SMT-LIB) compliant solvers with minimal effort and no modifications to existing code. Further, string constraint solvers that are not fully SMT-LIB compliant and require specific translations could be integrated with the addition of a single translation class and no modifications to existing code.