Abstract
We consider a class of arithmetic equations over the complete lattice of integers (extended with -∞ and ∞) and provide a polynomial time algorithm for computing least solutions. For systems of equations with addition and least upper bounds, this algorithm is a smooth generalization of the Bellman-Ford algorithm for computing the single source shortest path in presence of positive and negative edge weights. The method then is extended to deal with more general forms of operations as well as minima with constants. For the latter, a controlled widening is applied at loops where unbounded increase occurs. We apply this algorithm to construct a cubic time algorithm for the class of interval equations using least upper bounds, addition, intersection with constant intervals as well as multiplication.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Programs. In: Second Int. Symp. on Programming, Dunod, Paris, France, pp. 106–130 (1976)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE Analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Cousot, P., Cousot, R.: Comparison of the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In: JTASPEFL 1991, Bordeaux, vol. 74, pp. 107–110. BIGRE (1991)
Miné, A.: Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Miné, A.: Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2006)
Su, Z., Wagner, D.: A Class of Polynomially Solvable Range Constraints for Interval Analysis Without Widenings. Theor. Comput. Sci. (TCS) 345(1), 122–138 (2005)
Knuth, D.E.: A Generalization of Dijkstra’s algorithm. Information Processing Letters (IPL) 6(1), 1–5 (1977)
Gawlitza, T., Seidl, H.: Precise Fixpoint Computation Through Strategy Iteration. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 300–315. Springer, Heidelberg (2007)
Leroux, J., Sutre, G.: Accelerated Data-Flow Analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 184–199. Springer, Heidelberg (2007)
Seidl, H.: Least and Greatest Solutions of Equations over \(\cal N\). Nordic Journal of Computing (NJC) 3(1), 41–62 (1996)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms, 2nd edn. MIT Press, Cambridge (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Gawlitza, T., Leroux, J., Reineke, J., Seidl, H., Sutre, G., Wilhelm, R. (2009). Polynomial Precise Interval Analysis Revisited. In: Albers, S., Alt, H., Näher, S. (eds) Efficient Algorithms. Lecture Notes in Computer Science, vol 5760. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03456-5_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-03456-5_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03455-8
Online ISBN: 978-3-642-03456-5
eBook Packages: Computer ScienceComputer Science (R0)