Advertisement

Numerical Invariants via Abstract Machines

  • Zachary KincaidEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

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.

References

  1. 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_15CrossRefzbMATHGoogle Scholar
  2. 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)CrossRefGoogle Scholar
  3. 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. 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. 5.
    Berg, L.: Introduction to the Operational Calculus. North-Holland Publishing Co., Amsterdam (1967)zbMATHGoogle Scholar
  6. 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_16CrossRefGoogle Scholar
  7. 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_7CrossRefzbMATHGoogle Scholar
  8. 8.
    Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theor. Comp. Sci. 309(1), 413–468 (2003)MathSciNetCrossRefGoogle Scholar
  9. 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_29CrossRefGoogle Scholar
  10. 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_23CrossRefGoogle Scholar
  11. 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_49CrossRefzbMATHGoogle Scholar
  12. 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/BFb0028751CrossRefGoogle Scholar
  13. 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. 14.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)Google Scholar
  15. 15.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: POPL (1978)Google Scholar
  16. 16.
    Debray, S.K., Lin, N., Hermenegildo, M.V.: Task granularity analysis in logic programs. In: PLDI, pp. 174–188 (1990)Google Scholar
  17. 17.
    Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD (2015)Google Scholar
  18. 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_14CrossRefGoogle Scholar
  19. 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_10CrossRefGoogle Scholar
  20. 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_9CrossRefGoogle Scholar
  21. 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. 22.
    Humenberger, A., Jaroschek, M., Kovács, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: ISSAC (2017)Google Scholar
  23. 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. 24.
    Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL, pp. 529–540 (2014)Google Scholar
  25. 25.
    Kincaid, Z., Breck, J., Forouhi Boroujeni, A., Reps, T.: Compositional recurrence analysis revisited. In: PLDI (2017)Google Scholar
  26. 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. 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_42CrossRefGoogle Scholar
  28. 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_18CrossRefGoogle Scholar
  29. 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_10CrossRefGoogle Scholar
  30. 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. 31.
    Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)zbMATHGoogle Scholar
  32. 32.
    Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL (2004)Google Scholar
  33. 33.
    Reps, T., Thakur, A.: Automating abstract interpretation. In: VMCAI (2016)Google Scholar
  34. 34.
    Reps, T., Turetsky, E., Prabhu, P.: Newtonian program analysis via tensor product. In: POPL (2016)Google Scholar
  35. 35.
    Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: ISSAC, pp. 266–273 (2004)Google Scholar
  36. 36.
    Sebastiani, R., Tomasi, S.: Optimization in SMT with \(\cal{LA}(\mathbb{Q})\) cost functions. In: IJCAR, pp. 484–498 (2012)Google Scholar
  37. 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. 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. 39.
    Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM 28(3), 594–614 (1981)MathSciNetCrossRefGoogle Scholar
  40. 40.
    Tarjan, R.E.: A unified approach to path problems. J. ACM 28(3), 577–593 (1981)MathSciNetCrossRefGoogle Scholar
  41. 41.
    Thakur, A.: Symbolic abstraction: algorithms and applications. Ph.D. thesis, Computer Science Department, University of Wisconsin, Madison, WI, Technical report, 1812, August 2014Google Scholar
  42. 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_17CrossRefGoogle Scholar
  43. 43.
    Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Princeton UniversityPrincetonUSA

Personalised recommendations