[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Numerical Invariants via Abstract Machines

  • Conference paper
  • First Online:
Static Analysis (SAS 2018)

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

Included in the following conference series:

  • 1129 Accesses

Abstract

This paper presents an overview of a line of recent work on generating non-linear numerical invariants for loops and recursive procedures. The method is compositional in the sense that it operates by breaking the program into parts, analyzing each part independently, and then combining the results. The fundamental challenge is to devise an effective method for analyzing the behavior of a loop given the results of analyzing its body. The key idea is to separate the problem into two: first we approximate the loop dynamics by an abstract machine, and then symbolically compute the reachability relation of the abstract machine.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Similar content being viewed by others

Notes

  1. 1.

    For our purposes, the weaker hypothesis \(\mathcal {R}\![\![\gamma (M) \!]\!]^* \subseteq \mathcal {R}\![\![c\ell (M) \!]\!]\) is sufficient. We use equality to emphasize that \(\mathbf {M}\) is expected to be a class of machines that is easy to analyze.

References

  1. Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 221–237. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69166-2_15

    Chapter  MATH  Google Scholar 

  2. Ancourt, C., Coelho, F., Irigoin, F.: A modular static analysis approach to affine loop invariants detection. Electron. Notes Theor. Comput. Sci. 267(1), 3–16 (2010)

    Article  Google Scholar 

  3. Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: towards computer algebra support for fully automatic worst-case complexity analysis. CoRR abs/cs/0512056 (2005)

    Google Scholar 

  4. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI, pp. 203–213 (2001)

    Google Scholar 

  5. Berg, L.: Introduction to the Operational Calculus. North-Holland Publishing Co., Amsterdam (1967)

    MATH  Google Scholar 

  6. Biallas, S., Brauer, J., King, A., Kowalewski, S.: Loop leaping with closures. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 214–230. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33125-1_16

    Chapter  Google Scholar 

  7. Blanc, R., Henzinger, T.A., Hottelier, T., Kovács, L.: ABC: algebraic bound computation for loops. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 103–118. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_7

    Chapter  MATH  Google Scholar 

  8. Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theor. Comp. Sci. 309(1), 413–468 (2003)

    Article  MathSciNet  Google Scholar 

  9. Bozga, M., Gîrlea, C., Iosif, R.: Iterating octagons. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 337–351. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_29

    Chapter  Google Scholar 

  10. Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227–242. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_23

    Chapter  Google Scholar 

  11. Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 577–588. Springer, Heidelberg (2006). https://doi.org/10.1007/11787006_49

    Chapter  MATH  Google Scholar 

  12. Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028751

    Chapter  Google Scholar 

  13. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)

    Google Scholar 

  14. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)

    Google Scholar 

  15. Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: POPL (1978)

    Google Scholar 

  16. Debray, S.K., Lin, N., Hermenegildo, M.V.: Task granularity analysis in logic programs. In: PLDI, pp. 174–188 (1990)

    Google Scholar 

  17. Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD (2015)

    Google Scholar 

  18. Finkel, A., Leroux, J.: How to compose presburger-accelerations: applications to broadcast protocols. In: Agrawal, M., Seth, A. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36206-1_14

    Chapter  Google Scholar 

  19. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10

    Chapter  Google Scholar 

  20. Haase, C., Halfon, S.: Integer vector addition systems with states. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 112–124. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11439-2_9

    Chapter  Google Scholar 

  21. Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: Logic in Computer Science, pp. 530–539 (2018)

    Google Scholar 

  22. Humenberger, A., Jaroschek, M., Kovács, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: ISSAC (2017)

    Google Scholar 

  23. Humenberger, A., Jaroschek, M., Kovács, L.: Invariant generation for multi-path loops with polynomial assignments. In: VMCAI, pp. 226–246 (2018)

    Google Scholar 

  24. Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL, pp. 529–540 (2014)

    Google Scholar 

  25. Kincaid, Z., Breck, J., Forouhi Boroujeni, A., Reps, T.: Compositional recurrence analysis revisited. In: PLDI (2017)

    Google Scholar 

  26. Kincaid, Z., Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. PACMPL 2(POPL), 54:1–54:33 (2018)

    Google Scholar 

  27. Konečný, F.: PTIME computation of transitive closures of octagonal relations. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 645–661. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_42

    Chapter  Google Scholar 

  28. Kovács, L.: Reasoning algebraically about P-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 249–264. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_18

    Chapter  Google Scholar 

  29. Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 111–125. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88387-6_10

    Chapter  Google Scholar 

  30. Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL, pp. 607–618 (2014)

    Google Scholar 

  31. Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)

    MATH  Google Scholar 

  32. Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL (2004)

    Google Scholar 

  33. Reps, T., Thakur, A.: Automating abstract interpretation. In: VMCAI (2016)

    Google Scholar 

  34. Reps, T., Turetsky, E., Prabhu, P.: Newtonian program analysis via tensor product. In: POPL (2016)

    Google Scholar 

  35. Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: ISSAC, pp. 266–273 (2004)

    Google Scholar 

  36. Sebastiani, R., Tomasi, S.: Optimization in SMT with \(\cal{LA}(\mathbb{Q})\) cost functions. In: IJCAR, pp. 484–498 (2012)

    Google Scholar 

  37. Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: CAV, pp. 745–761 (2014)

    Google Scholar 

  38. Sinn, M., Zuleger, F., Veith, H.: Difference constraints: an adequate abstraction for complexity analysis of imperative programs. In: FMCAD, pp. 144–151 (2015)

    Google Scholar 

  39. Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM 28(3), 594–614 (1981)

    Article  MathSciNet  Google Scholar 

  40. Tarjan, R.E.: A unified approach to path problems. J. ACM 28(3), 577–593 (1981)

    Article  MathSciNet  Google Scholar 

  41. Thakur, A.: Symbolic abstraction: algorithms and applications. Ph.D. thesis, Computer Science Department, University of Wisconsin, Madison, WI, Technical report, 1812, August 2014

    Google Scholar 

  42. Thakur, A., Reps, T.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 174–192. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_17

    Chapter  Google Scholar 

  43. Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Princeton University, Princeton, USA

    Zachary Kincaid

Authors
  1. Zachary Kincaid
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zachary Kincaid .

Editor information

Editors and Affiliations

  1. Universität Freiburg, Freiburg, Germany

    Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kincaid, Z. (2018). Numerical Invariants via Abstract Machines. In: Podelski, A. (eds) Static Analysis. SAS 2018. Lecture Notes in Computer Science(), vol 11002. Springer, Cham. https://doi.org/10.1007/978-3-319-99725-4_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99725-4_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99724-7

  • Online ISBN: 978-3-319-99725-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation