Analysing all polynomial equations in ℤ2w

Helmut Seidl; Andrea Flexeder; Michael Petter

doi:10.1007/978-3-540-69166-2_20

Analysing all polynomial equations in ℤ_2w

Helmut Seidl, Andrea Flexeder, Michael Petter

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Scopus citations

Abstract

In this paper, we present methods for checking and inferring all valid polynomial relations in ℤ_2w. In contrast to the infinite field ℚ, ℤ_2w, is finite and hence allows for finitely many polynomial functions only. In this paper we show, that checking the validity of a polynomial invariant over is, though decidable, only PSPACE-complete. Apart from the impracticable algorithm for the theoretical upper bound, we present a feasible algorithm for verifying polynomial invariants over ℤ_2w which runs in polynomial time if the number of program variables is bounded by a constant. In this case, we also obtain a polynomial-time algorithm for inferring all polynomial relations. In general, our approach provides us with a feasible algorithm to infer all polynomial invariants up to a low degree.

Original language	English
Title of host publication	Static Analysis - 15th International Symposium, SAS 2008, Proceedings
Pages	299-314
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-540-69166-2_20
State	Published - 2008
Event	15th International Static Analysis Symposium, SAS 2008 - Valencia, Spain Duration: 16 Jul 2008 → 18 Jul 2008

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5079 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	15th International Static Analysis Symposium, SAS 2008
Country/Territory	Spain
City	Valencia
Period	16/07/08 → 18/07/08

Access to Document

10.1007/978-3-540-69166-2_20

Cite this

Seidl, H., Flexeder, A., & Petter, M. (2008). Analysing all polynomial equations in ℤ_2w. In Static Analysis - 15th International Symposium, SAS 2008, Proceedings (pp. 299-314). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5079 LNCS). https://doi.org/10.1007/978-3-540-69166-2_20

@inproceedings{a25dbe6f4ba04a33a46925fb351ef325,

title = "Analysing all polynomial equations in ℤ2w",

abstract = "In this paper, we present methods for checking and inferring all valid polynomial relations in ℤ2w. In contrast to the infinite field ℚ, ℤ2w, is finite and hence allows for finitely many polynomial functions only. In this paper we show, that checking the validity of a polynomial invariant over is, though decidable, only PSPACE-complete. Apart from the impracticable algorithm for the theoretical upper bound, we present a feasible algorithm for verifying polynomial invariants over ℤ2w which runs in polynomial time if the number of program variables is bounded by a constant. In this case, we also obtain a polynomial-time algorithm for inferring all polynomial relations. In general, our approach provides us with a feasible algorithm to infer all polynomial invariants up to a low degree.",

author = "Helmut Seidl and Andrea Flexeder and Michael Petter",

year = "2008",

doi = "10.1007/978-3-540-69166-2_20",

language = "English",

isbn = "3540691634",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "299--314",

booktitle = "Static Analysis - 15th International Symposium, SAS 2008, Proceedings",

note = "15th International Static Analysis Symposium, SAS 2008 ; Conference date: 16-07-2008 Through 18-07-2008",

}

Seidl, H, Flexeder, A & Petter, M 2008, Analysing all polynomial equations in ℤ_2w. in Static Analysis - 15th International Symposium, SAS 2008, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5079 LNCS, pp. 299-314, 15th International Static Analysis Symposium, SAS 2008, Valencia, Spain, 16/07/08. https://doi.org/10.1007/978-3-540-69166-2_20

Analysing all polynomial equations in ℤ_2w. / Seidl, Helmut; Flexeder, Andrea; Petter, Michael.
Static Analysis - 15th International Symposium, SAS 2008, Proceedings. 2008. p. 299-314 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5079 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Analysing all polynomial equations in ℤ2w

AU - Seidl, Helmut

AU - Flexeder, Andrea

AU - Petter, Michael

PY - 2008

Y1 - 2008

N2 - In this paper, we present methods for checking and inferring all valid polynomial relations in ℤ2w. In contrast to the infinite field ℚ, ℤ2w, is finite and hence allows for finitely many polynomial functions only. In this paper we show, that checking the validity of a polynomial invariant over is, though decidable, only PSPACE-complete. Apart from the impracticable algorithm for the theoretical upper bound, we present a feasible algorithm for verifying polynomial invariants over ℤ2w which runs in polynomial time if the number of program variables is bounded by a constant. In this case, we also obtain a polynomial-time algorithm for inferring all polynomial relations. In general, our approach provides us with a feasible algorithm to infer all polynomial invariants up to a low degree.

AB - In this paper, we present methods for checking and inferring all valid polynomial relations in ℤ2w. In contrast to the infinite field ℚ, ℤ2w, is finite and hence allows for finitely many polynomial functions only. In this paper we show, that checking the validity of a polynomial invariant over is, though decidable, only PSPACE-complete. Apart from the impracticable algorithm for the theoretical upper bound, we present a feasible algorithm for verifying polynomial invariants over ℤ2w which runs in polynomial time if the number of program variables is bounded by a constant. In this case, we also obtain a polynomial-time algorithm for inferring all polynomial relations. In general, our approach provides us with a feasible algorithm to infer all polynomial invariants up to a low degree.

UR - http://www.scopus.com/inward/record.url?scp=48949090135&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-69166-2_20

DO - 10.1007/978-3-540-69166-2_20

M3 - Conference contribution

AN - SCOPUS:48949090135

SN - 3540691634

SN - 9783540691631

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 299

EP - 314

BT - Static Analysis - 15th International Symposium, SAS 2008, Proceedings

T2 - 15th International Static Analysis Symposium, SAS 2008

Y2 - 16 July 2008 through 18 July 2008

ER -