Polynomial constants are decidable

Markus Müller-Olm, Helmut Seidl

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

31 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationStatic Analysis - 9th International Symposium, SAS 2002 Madrid, Spain, September 17-20, 2002 Proceedings
EditorsManuel V. Hermenegildo, German Puebla
PublisherSpringer Verlag
Pages4-19
Number of pages16
ISBN (Print)3540442359
DOIs
StatePublished - 2002
Externally publishedYes
Event9th International Static Analysis Symposium, SAS 2002 - Madrid, Spain
Duration: 17 Sep 200220 Sep 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2477
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Static Analysis Symposium, SAS 2002
Country/TerritorySpain
CityMadrid
Period17/09/0220/09/02

Fingerprint

Dive into the research topics of 'Polynomial constants are decidable'. Together they form a unique fingerprint.

Cite this