Abstract
We give a simple formulation of Karr’s algorithm for computing all affine relationships in affine programs. This simplified algorithm runs in time \(\mathcal{O}(nk^{3})\) where n is the program size and k is the number of program variables assuming unit cost for arithmetic operations. This improves upon the original formulation by a factor of k. Moreover, our re-formulation avoids exponential growth of the lengths of intermediately occurring numbers (in binary representation) and uses less complicated elementary operations. We also describe a generalization that determines all polynomial relations up to degree d in time \(\mathcal{O}(nk^{3d})\).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bagnara, R., Hill, P., Ricci, E., Zaffanella, E.: Precise Widening Operators for Convex Polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337–354. Springer, Heidelberg (2003)
Cousot, P., Cousot, R.: Abstract Interpretation:A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: 4th POPL (1977)
Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints among Variables of a Program. In: 5th POPL, pp. 84–97 (1978)
Gulwani, S., Necula, G.: Discovering Affine Equalities Using Random Interpretation. In: 30th POPL, pp. 74–84 (2003)
Hecht, M.S.: Flow analysis of computer programs. Elsevier North-Holland, Amsterdam (1977)
Karr, M.: Affine Relationships Among Variables of a Program. Acta Inf. 6, 133–151 (1976)
Leroux, J.: Algorithmique de la Vérification des Systèmes à Compteurs: Approximation et Accélération. PhD thesis, Ecole Normale Supérieure de Cachan (2003)
Müller-Olm, M., Rüthing, O.: The Complexity of Constant Propagation. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 190–205. Springer, Heidelberg (2001)
Müller-Olm, M., Seidl, H.: Computing Polynomial Program Invariants (2003) (submitted)
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., Seidl, H.: Precise Interprocedural Analysis through Linear Algebra. In: 31st POPL, pp. 330–341 (2004)
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller-Olm, M., Seidl, H. (2004). A Note on Karr’s Algorithm. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds) Automata, Languages and Programming. ICALP 2004. Lecture Notes in Computer Science, vol 3142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27836-8_85
Download citation
DOI: https://doi.org/10.1007/978-3-540-27836-8_85
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22849-3
Online ISBN: 978-3-540-27836-8
eBook Packages: Springer Book Archive