Two-sided unification is NP-complete.
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.Full text of the paper in pdf
Proceedings of the 28th International Workshop on Unification (UNIF-2014), RISC-Linz Report Series, 2014, JKU Linz, Vienna, Austria, vol. 6, p. 55-61.