Rule-based Word Equation Solving

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

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

1 Citationer (Scopus)

Abstrakt

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.
OriginalsprogEngelsk
TitelFormaliSE '20: Proceedings of the 8th International Conference on Formal Methods in Software
Antal sider11
ForlagAssociation for Computing Machinery
Publikationsdato2020
Sider87–97
Artikelnummer3391556
ISBN (Trykt)978-1-4503-7071-4
DOI
StatusUdgivet - 2020
BegivenhedInternational Conference on Formal Methods in Software Engineering. - Seoul, Sydkorea
Varighed: 1 okt. 202031 okt. 2020
Konferencens nummer: 8th

Konference

KonferenceInternational Conference on Formal Methods in Software Engineering.
Nummer8th
LandSydkorea
BySeoul
Periode01/10/202031/10/2020

Citationsformater