Simple and Efficient Algorithms for Octagons

  • Aziem Chawdhary
  • Ed Robbins
  • Andy King
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)


The numerical domain of Octagons can be viewed as an exercise in simplicity: it trades expressiveness for efficiency and ease of implementation. The domain can represent unary and binary constraints where the coefficients are + 1 or − 1, so called octagonal constraints, and comes with operations that have cubic complexity. The central operation is closure which computes a canonical form by deriving all implied octagonal constraints from a given octagonal system. This paper investigates the role of incrementality, namely closing a system where only one constraint has been changed, which is a dominating use-case. We present two new incremental algorithms for closure both of which are conceptually simple and computationally efficient, and argue their correctness.


Model Check Unary Constraint Canonical Representation Short Path Algorithm Incremental Algorithm 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness. Formal Methods in System Design 35(3), 279–323 (2009)CrossRefzbMATHGoogle Scholar
  2. 2.
    Baykan, C.A., Fox, M.S.: Spatial Synthesis by Disjunctive Constraint Satisfaction. Artificial Intelligence for Engineering, Design, Analysis and Manufacturing 11(4), 245–262 (1997)CrossRefGoogle Scholar
  3. 3.
    Bellman, R.: On a Routing Problem. Quarterly of Applied Mathematics 16, 87–90 (1958)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O’Hearn, P.: Variance Analyses from Invariance Analyses. In: POPL, pp. 211–224. ACM (2007)Google Scholar
  5. 5.
    Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints among Variables of a Program. In: POPL, pp. 84–97. ACM Press (1978)Google Scholar
  7. 7.
    Floyd, R.W.: Algorithm 97: Shortest Path. CACM 5(6), 345 (1962)CrossRefGoogle Scholar
  8. 8.
    Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically Refining Abstract Interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 443–458. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Harrison, W.H.: Compiler Analysis for the Value Ranges of Variables. IEEE Transactions on Software Engineering SE-3(3), 243–250 (1977)Google Scholar
  10. 10.
    Harvey, W., Stuckey, P.J.: A Unit Two Variable Per Inequality Integer Constraint Solver for Constraint Logic Programming. In: Patel, M., Kotagiri, R. (eds.) Twentieth Australasian Computer Science Conference, pp. 102–111. Macquarie University (1997), Also available as TR 95/30 from University of MelbourneGoogle Scholar
  11. 11.
    Jeannet, B., Miné, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    Jhala, R., Majumdar, R.: Software Model Checking. ACM Computing Surveys 41(4), 21:1–21:54 (2009)Google Scholar
  13. 13.
    Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic Strengthening for Shape Analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 419–436. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Miné, A.: A New Numerical Abstract Domain Based on Difference-Bound Matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Miné, A.: Weakly Relational Numerical Abstract Domains. PhD thesis, École Polytechnique (2004),
  16. 16.
    Miné, A.: The Octagon Abstract Domain. HOSC 19(1), 31–100 (2006)zbMATHGoogle Scholar
  17. 17.
    Robbins, E., Howe, J.M., King, A.: Theory Propagation and Reification. Science of Computer Programming (to appear),
  18. 18.
    Simon, A., King, A.: Taming the Wrapping of Integer Arithmetic. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 121–136. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  19. 19.
    Simon, A., King, A., Howe, J.M.: The Two Variable Per Inequality Abstract Domain. HOSC 31(1), 182–196 (2010), Google Scholar
  20. 20.
    Warshall, S.: A Theorem on Boolean Matrices. JACM 9(1), 11–12 (1962)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Aziem Chawdhary
    • 1
  • Ed Robbins
    • 1
  • Andy King
    • 1
  1. 1.University of KentUK

Personalised recommendations