Is it possible to unify sequential programs.
We introduce a first-order model of imperative sequential programs and set up formally the unification problem in this model: given a pair of programs $\pi_1$ and $\pi_2$ find a pair of substitutions $(\theta_1,\theta_2)$ such that the instances $\pi_1\theta_1$ and $\pi_2\theta_2$ of these programs are equivalent, i.e. compute the same function. Since functional equivalence of programs is undecidable, we choose its decidable approximation - a strong equivalence, - which is well-known in theory of program schemata. Our main result is a polynomial time unification algorithm for sequential programs w.r.t. strong equivalence of programs.
Proceedings of the 27-th International Workshop on Unification, June 26, 2013, Eindhoven, EPiC Series, 2013, vol. 123, pp. 36-46.