cell morphing: from array programs to array-free horn clauses

a paper by d. monniaux, l. gonnord

From our programs with arrays, we generate nonlinear Horn clauses over scalar variables only,in a common format with clear and unambiguous logical semantics, for which there exist several solvers. We thus avoid the use of solvers operating over arrays, which are still very immature.