Markus Müller-Olm and Helmut Seidl. Polynomial Constants Are Decidable. In Manuel V. Hermenegildo and Germán Puebla, editors, Static Analysis, volume 2477 of Lecture Notes in Computer Science, pages 4-19, Madrid, Spain, September 2002. Springer.

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.

Download: PDF Reference: Bibtex The original publication is available at