Supercompiling String Programs Using Word Equations as Constraints

TL;DR

This paper presents a unified framework combining supercompilation and quadratic word equation solving for string programs, enabling more effective program analysis and specialization.

Contribution

It introduces a parameterized scheme that integrates program supercompilation with word equation solving using string constraints, unifying two analysis methods.

Findings

The scheme effectively combines supercompilation and word equation solving.

It handles string constraints with inequalities on regular patterns.

The integrated approach improves program analysis capabilities.

Abstract

We describe a general parameterized scheme of program and constraint analyses allowing us to specify both the program specialization method known as Turchin's supercompilation and Hmelevskii's algorithm solving the quadratic word equations. The scheme is specified for both sorts of the analysis and works in a joint algorithm in which these two sorts of the analysis are used together. The word equations and the inequalities on regular patterns are used as the string constraint language in the algorithm.