Markus Müller-Olm and Helmut Seidl. Polynomial Constants are Decidable. , volume 02-09 of Forschungsbericht, 2002. Universität Trier, Mathematik/Informatik.

Constant propagation aims at identifying expressions that always yield a unique constant value at run-time. It is well-known that constant propagation is undecidable for programs working on integers even if guards are ignored as in non-deterministic flow graphs. We show that polynomial constants are decidable in non-deterministic flow graphs. In polynomial constant propagation, assignment statements that use the operators +, -,* are interpreted exactly but all assignments that use other operators are conservatively interpreted as non-deterministic assignments. We present a generic algorithm for constant propagation via a symbolic weakest precondition computation and show how this generic algorithm can be instantiated for polynomial constant propagation by exploiting techniques from computable ring theory.

Reference: Bibtex