Abstract
In this paper, we present methods for checking and inferring all valid polynomial relations in \({\mathbb Z_{2^w}}\). In contrast to the infinite field ℚ, \({\mathbb Z_{2^w}}\) 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 \({\mathbb Z_{2^w}}\) 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 \({\mathbb Z_{2^w}}\) 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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Becker, T., Weispfenning, V.: Gröbner Bases – a computational approach to commutative algebra. Springer, New York (1993)
Colon, M.: Polynomial approximations of the relational semantics of imperative programs. Science of Computer Programming 64, 76–96 (2007)
Hungerbühler, N., Specker, E.: A generalization of the smarandache function to several variables. Integers: Electronic Journal Combinatorial Number Theory 6 (2006)
Karr, M.: Affine Relationships Among Variables of a Program. Acta Informatica 6, 133–151 (1976)
Matsumura, H.: Commutative Ring Theory. Cambridge University Press, Cambridge (1989)
Müller-Olm, M., Rüthing, O.: On the complexity of constant propagation. In: Sands, D. (ed.) ESOP 2001 and ETAPS 2001. LNCS, vol. 2028, Springer, Heidelberg (2001)
Müller-Olm, M., Seidl, H.: Polynomial Constants are Decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 4–19. Springer, Heidelberg (2002)
Müller-Olm, M., Petter, M., Seidl, H.: Interprocedurally analyzing polynomial identities. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 50–67. Springer, Heidelberg (2006)
Müller-Olm, M., Seidl, H.: Computing Polynomial Program Invariants. Information Processing Letters (IPL) 91(5), 233–244 (2004)
Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444. Springer, Heidelberg (2005)
Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Transactions on Programming Languages and Systems (TOPLAS) 29(5) (2007)
Petter, M.: Berechnung von polynomiellen Invarianten. Master’s thesis, Technische Universität München, München (2004)
Rodríguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)
Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Science of Computer Programming 64, 54–75 (2007)
Sankaranarayanan, S., Henry, Z.M., Sipma, B.: Non-linear loop invariant generation using gröbner bases. In: ACM SIGPLAN Principles of Programming Languages (POPL) (2004)
Shekhar, N., Kalla, P., Enescu, F., Gopalakrishnan, S.: Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebra. In: International Conference on Computer-Aided Design (ICCAD), pp. 291–296 (2005)
Singmaster, D.: On polynomial functions (mod m). Journal of Number Theory 6, 345–352 (1974)
Wienand, O.: The Groebner basis of the ideal of vanishing polynomials. Journal of Symbolic Computation (JSC) (to appear, 2007); Preprint in arxiv math.AC/0801.1177
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seidl, H., Flexeder, A., Petter, M. (2008). Analysing All Polynomial Equations in \({\mathbb Z_{2^w}}\) . In: Alpuente, M., Vidal, G. (eds) Static Analysis. SAS 2008. Lecture Notes in Computer Science, vol 5079. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69166-2_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-69166-2_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69163-1
Online ISBN: 978-3-540-69166-2
eBook Packages: Computer ScienceComputer Science (R0)