Rule-based Word Equation Solving

Joel Day, Mitja Kulczynski, Florin Manea, Dirk Nowotka, Danny Bøgsted Poulsen

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

3 Citations (Scopus)


We present a transformation-system-based technique in the frame-work 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. To improve the efficiency of our transformation-system approach we integrate existing successful string solvers, which are called based on several heuristics. The experimental evaluation we performed shows that integrating our technique as an inprocessing step improves in general the performance of existing solvers.
Original languageEnglish
Title of host publicationFormaliSE '20: Proceedings of the 8th International Conference on Formal Methods in Software
Number of pages11
PublisherAssociation for Computing Machinery
Publication date2020
Article number3391556
ISBN (Print)978-1-4503-7071-4
Publication statusPublished - 2020
EventInternational Conference on Formal Methods in Software Engineering. - Seoul, Korea, Republic of
Duration: 1 Oct 202031 Oct 2020
Conference number: 8th


ConferenceInternational Conference on Formal Methods in Software Engineering.
Country/TerritoryKorea, Republic of

Cite this