Advertisement

The Abstract Domain of Segmented Ranking Functions

  • Caterina Urban
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7935)

Abstract

We present a parameterized abstract domain for proving program termination by abstract interpretation. The domain automatically synthesizes piecewise-defined ranking functions and infers sufficient conditions for program termination. The analysis uses over-approximations but we prove its soundness, meaning that all program executions respecting these sufficient conditions are indeed terminating.

The abstract domain is parameterized by a numerical abstract domain for environments and a numerical abstract domain for functions. This parameterization allows to easily tune the trade-off between precision and cost of the analysis. We describe an instantiation of this generic domain with intervals and affine functions. We define all abstract operators, including widening to ensure convergence.

To illustrate the potential of the proposed framework, we have implemented a research prototype static analyzer, for a small imperative language, that yielded interesting preliminary results.

Keywords

Ranking Function Abstract Interpretation Invariance Analysis Abstract Property Abstract Domain 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-Form Upper Bounds in Static Cost Analysis. J. Autom. Reasoning 46(2), 161–203 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117–133. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O’Hearn, P.W.: Variance Analyses from Invariance Analyses. In: POPL, pp. 211–224 (2007)Google Scholar
  4. 4.
    Bourdoncle, F.: Efficient Chaotic Iteration Strategies with Widenings. In: FMPA, pp. 128–141 (1993)Google Scholar
  5. 5.
    Bradley, A.R., Manna, Z., Sipma, H.B.: The Polyranking Principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1349–1361. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving Conditional Termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 328–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Cook, B., Podelski, A., Rybalchenko, A.: TERMINATOR: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Cook, B., Podelski, A., Rybalchenko, A.: Proving Program Termination. Commun. ACM 54(5), 88–98 (2011)CrossRefGoogle Scholar
  9. 9.
    Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Programs. In: Proceedings of the Second International Symposium on Programming, pp. 106–130 (1976)Google Scholar
  10. 10.
    Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL, pp. 238–252 (1977)Google Scholar
  11. 11.
    Cousot, P., Cousot, R.: Abstract Interpretation and Application to Logic Programs. J. Log. Program. 13(2&3), 103–179 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Cousot, P., Cousot, R.: Abstract Interpretation Frameworks. J. Log. Comput. 2(4), 511–547 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 13.
    Cousot, P., Cousot, R.: Higher Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection, and PER Analysis. In: ICCL, pp. 95–112 (1994)Google Scholar
  14. 14.
    Cousot, P., Cousot, R.: An Abstract Interpretation Framework for Termination. In: POPL, pp. 245–258 (2012)Google Scholar
  15. 15.
    Cousot, P., Cousot, R., Logozzo, F.: A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis. In: POPL, pp. 105–118 (2011)Google Scholar
  16. 16.
    Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: POPL, pp. 84–96 (1978)Google Scholar
  17. 17.
    Feret, J.: The Arithmetic-Geometric Progression Abstract Domain. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 42–58. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  18. 18.
    Floyd, R.W.: Assigning Meanings to Programs. In: Proceedings of Symposium on Applied Mathematics, vol. 19, pp. 19–32 (1967)Google Scholar
  19. 19.
    Jeannet, B.: Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems. Formal Methods in System Design 23(1), 5–37 (2003)zbMATHCrossRefGoogle Scholar
  20. 20.
    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
  21. 21.
    Miné, A.: The Octagon Abstract Domain. HOSC 19(1), 31–100 (2006)zbMATHGoogle Scholar
  22. 22.
    Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  23. 23.
    Podelski, A., Rybalchenko, A.: Transition Invariants. In: LICS, pp. 32–41 (2004)Google Scholar
  24. 24.
    Rival, X., Mauborgne, L.: The Trace Partitioning Abstract Domain. ACM Transactions on Programming Languages and Systems 29(5) (2007)Google Scholar
  25. 25.
    Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop Summarization and Termination Analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 81–95. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  26. 26.
    Turing, A.: Checking a Large Routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67–69 (1948)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Caterina Urban
    • 1
  1. 1.CNRS - INRIAÉcole Normale SupérieureParisFrance

Personalised recommendations