Skip to main content
SpringerLink
Log in

Compact Difference Bound Matrices

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10695))

Included in the following conference series:

Abstract

The Octagon domain, which tracks a restricted class of two-variable inequalities, is the abstract domain of choice for many applications because its domain operations are either quadratic or cubic in the number of program variables. Octagon constraints are classically represented using a Difference Bound Matrix (DBM), where the entries in the DBM store bounds c for inequalities of the form \(x_i - x_j \leqslant c\), \(x_i + x_j \leqslant c\) or \(-x_i - x_j \leqslant c\). The size of such a DBM is quadratic in the number of variables, giving a representation which can be excessively large for number systems such as rationals. This paper proposes a compact representation for DBMs, in which repeated numbers are factored out of the DBM. The paper explains how the entries of a DBM are distributed, and how this distribution can be exploited to save space and significantly speed-up long-running analyses. Moreover, unlike sparse representations, the domain operations retain their conceptually simplicity and ease of implementation whilst reducing memory usage.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Allen, B., Munro, I.: Self-organizing binary search trees. J. ACM 25(4), 526–535 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness. Form. Methods Syst. Des. 35(3), 279–323 (2009)

    Article  MATH  Google Scholar 

  3. Banterle, F., Giacobazzi, R.: A fast implementation of the octagon abstract domain on graphics hardware. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 315–332. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74061-2_20

    Chapter  Google Scholar 

  4. Beckschulze, E., Kowalewski, S., Brauer, J.: Access-based localization for octagons. Electron. Notes Theor. Comput. Sci. 287, 29–40 (2012)

    Article  MATH  Google Scholar 

  5. Bellman, R.: On a routing problem. Q. Appl. Math. 16, 87–90 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  6. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI, pp. 196–207 (2003)

    Google Scholar 

  7. Briggs, P., Torczon, L.: An efficient representation for sparse sets. ACM Lett. Program. Lang. Syst. 2(1–4), 59–69 (1993)

    Article  Google Scholar 

  8. Bühler, D., Cuoq, P., Yakobowski, B., Lemerre, M., Maroneze, A., Perrelle, V., Prevosto, V.: The EVA Plug-in. CEA LIST, Software Reliability Laboratory, Saclay, France, F-91191 (2017). https://frama-c.com/download/frama-c-value-analysis.pdf

  9. Chawdhary, A., Robbins, E., King, A.: Simple and efficient algorithms for octagons. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 296–313. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12736-1_16

    Google Scholar 

  10. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_17

    Chapter  Google Scholar 

  11. Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Exploiting sparsity in difference-bound matrices. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 189–211. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_10

    Chapter  Google Scholar 

  12. Heo, K., Oh, H., Yang, H.: Learning a variable-clustering strategy for octagon from labeled data generated by a static analysis. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 237–256. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_12

    Chapter  Google Scholar 

  13. 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). https://doi.org/10.1007/978-3-642-02658-4_52

    Chapter  Google Scholar 

  14. Jourdan, J.-H.: Verasco: a formally verified C static analyzer. Ph.D. thesis, Université Paris Diderot (Paris 7) Sorbonne Paris Cité, May 2016

    Google Scholar 

  15. Lassez, J.-L., Huynh, T., McAloon, K.: Simplication and elimination of redundant linear arithmetic constraints. In: Constraint Logic Programming, pp. 73–87. MIT Press (1993)

    Google Scholar 

  16. Measche, M., Berthomieu, B.: Time Petri-nets for analyzing and verifying time dependent communication protocols. In: Rudin, H., West, C. (eds.) Protocol Specification, Testing and Verification III, pp. 161–172. North-Holland (1983)

    Google Scholar 

  17. Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique En Informatique (2004)

    Google Scholar 

  18. Miné, A.: The octagon abstract domain. HOSC 19(1), 31–100 (2006)

    MATH  Google Scholar 

  19. Nethercote, N.: Dynamic binary analysis and instrumentation. Ph.D. thesis, Trinity College, University of Cambridge (2004)

    Google Scholar 

  20. Oh, H., Heo, K., Lee, W., Lee, W., Park, D., Kang, J., Yi, K.: Global sparse analysis framework. ACM TOPLAS 36(3), 8:1–8:44 (2014)

    Article  Google Scholar 

  21. Pavlov, I.: Lempel-Ziv-Markov chain algorithm CPU benchmarking (2017). http://www.7-cpu.com/

  22. Ruggieri, S.: On computing the semi-sum of two integers. Inf. Process. Lett. 87(2), 67–71 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  23. Singh, G., Püschel, M., Vechev, M.: Making numerical program analysis fast. In: PLDI, pp. 303–313. ACM Press (2015)

    Google Scholar 

  24. Venet, A., Brat, G. Precise and efficient static array bound checking for large embedded C programs. In: PLDI, pp. 31–242 (004)

    Google Scholar 

  25. Weidendorfer, J., Kowarschik, M., Trinitis, C.: A tool suite for simulation based analysis of memory access behavior. In: Bubak, M., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds.) ICCS 2004. LNCS, vol. 3038, pp. 440–447. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24688-6_58

    Chapter  Google Scholar 

  26. Williams Jr., L.F.: A modification to the half-interval search (binary search) method. In: Proceedings of the 14th ACM Southeast Conference, pp. 95–101 (1976)

    Google Scholar 

Download references

Acknowledgements

We thank Colin King at Canonical Limited for his tireless patience and help with the performance analysis which underpinned this work.

Author information

Authors and Affiliations

  1. University of Kent, Canterbury, CT2 7NF, UK

    Aziem Chawdhary & Andy King

Authors
  1. Aziem Chawdhary
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andy King
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Aziem Chawdhary .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, Colorado, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Chawdhary, A., King, A. (2017). Compact Difference Bound Matrices. In: Chang, BY. (eds) Programming Languages and Systems. APLAS 2017. Lecture Notes in Computer Science(), vol 10695. Springer, Cham. https://doi.org/10.1007/978-3-319-71237-6_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-71237-6_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-71236-9

  • Online ISBN: 978-3-319-71237-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation