Abstract
The abstract domain of polyhedra is sufficiently expressive to be deployed in verification. One consequence of the richness of this domain is that long, possibly infinite, sequences of polyhedra can arise in the analysis of loops. Widening and narrowing have been proposed to infer a single polyhedron that summarises such a sequence of polyhedra. Motivated by precision losses encountered in verification, we explain how the classic widening/narrowing approach can be refined by an improved extrapolation strategy. The insight is to record inequalities that are thus far found to be unsatisfiable in the analysis of a loop. These so-called landmarks hint at the amount of widening necessary to reach stability. This extrapolation strategy, which refines widening with thresholds, can infer post-fixpoints that are precise enough not to require narrowing. Unlike previous techniques, our approach interacts well with other domains, is fully automatic, conceptually simple and precise on complex loops.
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. Science of Computer Programming 58(1-2), 28–56 (2005)
Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double desciption method. Formal Asp. Comput. 17(2), 222–257 (2005)
Benoy, P.M.: Polyhedral Domains for Abstract Interpretation in Logic Programming. PhD thesis, Computing Lab., Univ. of Kent, Canterbury, UK (January 2002)
Besson, F., Jensen, T., Talpin, J.-P.: Polyhedral analysis for synchronous languages. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 51–68. Springer, Heidelberg (1999)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002)
Bourdoncle, F.: Efficient Chaotic Iteration Strategies with Widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol. 735, pp. 128–141. Springer, Heidelberg (1993)
Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Programs. In: Second International Symposium on Programming, Dunod, Paris, France, pp. 106–130 (1976)
Cousot, P., Cousot, R.: Abstract Interpretation and Application to Logic Programs. Journal of Logic Programming 13(2-3), 103–179 (1992)
Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Constraints among Variables of a Program. In: Symposium on Principles of Programming Languages, Tucson, Arizona, pp. 84–97. ACM Press, New York (1978)
Dor, N., Rodeh, M., Sagiv, M.: Cleanness checking of string manipulations in C programs via integer analysis. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 194–212. Springer, Heidelberg (2001)
Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452–466. Springer, Heidelberg (2006)
Gulavani, B.S., Rajamani, S.K.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 474–488. Springer, Heidelberg (2006)
Halbwachs, N.: Détermination Automatique de Relations Linéaires Vérifiées par les Variables d’un Programme. Thèse de 3ème icle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France (March 1979)
Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of Real-Time Systems using Linear Relation Analysis. Formal Methods in System Design 11(2), 157–185 (1997)
Harvey, W.: Computing Two-Dimensional Integer Hulls. SIAM Journal on Computing 28(6), 2285–2299 (1999)
Heintze, N., Tardieu, O.: Ultra-fast Aliasing Analysis using CLA: A Million Lines of C Code in a Second. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 254–263 (2001)
Miné, A.: The Octagon Abstract Domain. In: Eighth Working Conference on Reverse Engineering, pp. 310–319. IEEE Computer Society Press, Los Alamitos (2001)
Sankaranarayanan, S., Colón, M., Sipma, H.B., Manna, Z.: Efficient strongly relational polyhedral analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 111–125. Springer, Heidelberg (2005)
Simon, A., King, A.: Analyzing string buffers in C. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 365–379. Springer, Heidelberg (2002)
Simon, A., King, A.: Exploiting sparsity in polyhedral analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 336–351. Springer, Heidelberg (2005)
Simon, A., King, A., Howe, J.M.: Two Variables per Linear Inequality as an Abstract Domain. In: Leuschel, M.A. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 71–89. Springer, Heidelberg (2003)
Steensgaard, B.: Points-to Analysis in Almost Linear Time. In: Symposium on the Principles of Progamming Languages, pp. 32–41 (1996)
Su, Z., Wagner, D.: A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings. Theor. Comput. Sci. 345(1), 122–138 (2005)
Wagner, D.: Static analysis and computer security: New techniques for software assurance. PhD thesis, University of California at Berkeley (December 2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Simon, A., King, A. (2006). Widening Polyhedra with Landmarks. In: Kobayashi, N. (eds) Programming Languages and Systems. APLAS 2006. Lecture Notes in Computer Science, vol 4279. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11924661_11
Download citation
DOI: https://doi.org/10.1007/11924661_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48937-5
Online ISBN: 978-3-540-48938-2
eBook Packages: Computer ScienceComputer Science (R0)