Write a Blog >>
ICSE 2020
Wed 24 June - Thu 16 July 2020

We present a transformation-system-based technique in the framework of string solving, by reformulating a classical combinatorics on words result, the Lemma of Levi. We further enrich the induced rules by simplification steps based on results from the combinatorial theory of word equations, as well as by the addition of linear length constraints. This transformation-system approach cannot solve all equations efficiently by itself, so our final approach integrates existing string solvers, which are called based on heuristics. Experimental evaluation shows that this technique is useful as an inprocessing method for existing solvers.