Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2015: Static Analysis pp 293–311Cite as

A Forward Analysis for Recurrent Sets

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9291))

Abstract

Non-termination of structured imperative programs is primarily due to infinite loops. An important class of non-terminating loop behaviors can be characterized using the notion of recurrent sets. A recurrent set is a set of states from which execution of the loop cannot or might not escape. Existing analyses that infer recurrent sets to our knowledge rely on one of: the combination of forward and backward analyses, quantifier elimination, or SMT-solvers. We propose a purely forward abstract interpretation–based analysis that can be used together with a possibly complicated abstract domain where none of the above is readily available. The analysis searches for a recurrent set of every individual loop in a program by building a graph of abstract states and analyzing it in a novel way. The graph is searched for a witness of a recurrent set that takes the form of what we call a recurrent component which is somewhat similar to the notion of an end component in a Markov decision process.

This is a preview of subscription content, 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

Learn about institutional subscriptions

References

  1. http://azure.microsoft.com/blog/2014/11/19/update-on-azure-storage-service-interruption. Accessed March 2015

  2. http://www.zuneboards.com/forums/showthread.php?t=38143. Accessed March 2015

  3. http://www.cs.tau.ac.il/~tvla/. Accessed March 2015

  4. http://www.key-project.org/nonTermination/. Accessed March 2015

  5. http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/file/d085ae59ef47/C/Ultimate. Accessed March 2015

  6. http://aprove.informatik.rwth-aachen.de/eval/JBC-Nonterm/. Accessed June 2015

  7. Arnold, G., Manevich, R., Sagiv, M., Shaham, R.: Combining shape analyses by intersecting abstractions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 33–48. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)

    Google Scholar 

  9. Bakhirkin, A., Berdine, J., Piterman, N.: A forward analysis for recurrent sets. Technical report CS-15-001, University of Leicester (2015)

    Google Scholar 

  10. Berdine, J., Cook, B., Distefano, D., O’Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386–400. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869–882. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 123–141. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.: Proving nontermination via safety. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 156–171. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  14. Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.W.: Disproving termination with overapproximation. In: FMCAD, pp. 67–74. IEEE (2014)

    Google Scholar 

  15. Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011)

    Article  Google Scholar 

  16. Cook, B., See, A., Zuleger, F.: Ramsey vs. Lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 47–61. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) POPL, pp. 84–96. ACM Press (1978)

    Google Scholar 

  18. Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 184–191. Springer, Heidelberg (2014)

    Google Scholar 

  19. Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.G.: Proving non-termination. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 147–158. ACM (2008)

    Google Scholar 

  20. Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365–380. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  21. Kleene, S.: Introduction to Metamathematics, 2nd edn. Literary Licensing, LLC, Amsterdam (1987)

    Google Scholar 

  22. Larraz, D., Nimkar, K., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving non-termination using Max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779–796. Springer, Heidelberg (2014)

    Google Scholar 

  23. Lev-Ami, T., Manevich, R., Sagiv, S.: TVLA: a system for generating abstract interpreters. In: Jacquart, R. (ed.) IFIP 2004. IFIP, vol. 156, pp. 367–375. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  24. Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 380–398. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  26. Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)

    Article  Google Scholar 

  27. 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)

    Google Scholar 

  28. Velroyen, H., Rümmer, P.: Non-termination checking for imperative programs. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 154–170. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Acknowledgements

We thank Mooly Sagiv and Roman Manevich for the source code of TVLA. A. Bakhirkin is supported by a Microsoft Research PhD Scholarship.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Leicester, Leicester, UK

    Alexey Bakhirkin & Nir Piterman

  2. Microsoft Research, Cambridge, UK

    Josh Berdine

Authors
  1. Alexey Bakhirkin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Josh Berdine
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nir Piterman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Josh Berdine .

Editor information

Editors and Affiliations

  1. Université Rennes 1, Rennes, France

    Sandrine Blazy

  2. Inria, Rennes, France

    Thomas Jensen

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bakhirkin, A., Berdine, J., Piterman, N. (2015). A Forward Analysis for Recurrent Sets. In: Blazy, S., Jensen, T. (eds) Static Analysis. SAS 2015. Lecture Notes in Computer Science(), vol 9291. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48288-9_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48288-9_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48287-2

  • Online ISBN: 978-3-662-48288-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation