Quantifier Elimination in Automatic Loop Parallelization

We present an application of quantifier elimination techniques in the automatic par-allelization of nested loop programs. The technical goal is to simplify affine inequal-ities whose coefficients may be unevaluated symbolic constants. The values of these so-called structure parameters are determined at run time and reflect the problem size. Our purpose here is to make the research community of quantifier elimination, in a tutorial style, aware of our application domain –loop parallelization – and to highlight the rôle of quantifier elimination, as opposed to alternative techniques, in this domain. Technically, we focus on the elimination method of Weispfenning. Key words: loop parallelization, quantifier elimination