Polynomial Constants are Decidable

11 years 26 days ago
Polynomial Constants are Decidable
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.
Markus Müller-Olm, Helmut Seidl
Added 23 Dec 2010
Updated 23 Dec 2010
Type Journal
Year 2002
Authors Markus Müller-Olm, Helmut Seidl
Comments (0)