Advertisement

FuncTion: An Abstract Domain Functor for Termination

(Competition Contribution)
  • Caterina UrbanEmail author
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)

Abstract

FuncTion is a research prototype static analyzer designed for proving (conditional) termination of C programs. The tool automatically infers piecewise-defined ranking functions (and sufficient preconditions for termination) by means of abstract interpretation. It combines a variety of abstract domains in order to balance the precision and cost of the analysis.

References

  1. 1.
    Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Programs. In: International Symposium on Programming, pp. 106–130 (1976)Google Scholar
  2. 2.
    Cousot, P., Cousot, R.: An Abstract Interpretation Framework for Termination. In: POPL, pp. 245–258 (2012)Google Scholar
  3. 3.
    Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: POPL, pp. 84–96 (1978)Google Scholar
  4. 4.
    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
  5. 5.
    Miné, A.: The Octagon Abstract Domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)CrossRefzbMATHGoogle Scholar
  6. 6.
    Urban, C.: The abstract domain of segmented ranking functions. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 43–62. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  7. 7.
    Urban, C., Miné, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 412–431. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  8. 8.
    Urban, C., Miné, A.: A decision tree abstract domain for proving conditional termination. In: Müller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 302–318. Springer, Heidelberg (2014)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  1. 1.ÉNS and CNRS and INRIAPARIS Cedex 13France

Personalised recommendations