Paper Info
Title
Program Specialization as a Tool for Solving Word Equations.
Abstract
The paper focuses on the automatic generating of the witnesses for the word equation satisfiability problem by means of specializing an interpreter which tests whether a composition of variable substitutions of a given word equation system produces its solution. We specialize such an interpreter w.r.t. the equation system, while the substitutions are unknown. We show that several variants of such interpreters, when specialized using the basic unfold/fold specialization methods, are able to construct the whole solution sets for some classes of the word equations whose left- and right-hand sides share variables. We prove that the specialization process wrt the constructed interpreters gives a simple syntactic criterion of the satisfiability of the equations considered, and show that the suggested approach can solve some equations not solvable by Z3str3 and CVC4, the widely-used SMT-solvers.
Year
DOI
Venue
2021
10.4204/EPTCS.341.4
European Joint Conferences on Theory And Practice of Software
DocType
ISSN
Citations 
Conference
EPTCS 341, 2021, pp. 42-72
0
PageRank 
References 
Authors
0.34
0
1
Name
Order
Citations
PageRank
Antonina Nepeivoda111.03