References

  1. Elvira Albert, Puri Arenas, Samir Genaim & Germán Puebla (2011): Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning 46(2), pp. 161–203, doi:10.1007/s10817-010-9174-1.
  2. Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin & Albert Rubio (2019): Resource Analysis driven by (Conditional) Termination Proofs. Theory and Practice of Logic Programming 19(5-6), pp. 722–739, doi:10.1017/S1471068419000152.
  3. Christophe Alias, Alain Darte, Paul Feautrier & Laure Gonnord (2010): Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In: Radhia Cousot & Matthieu Martel: Static Analysis Symposium, SAS'10, LNCS 6337. Springer, pp. 117–133, doi:10.1007/978-3-642-15769-1_8.
  4. Amir M. Ben-Amram, Jesús J. Doménech & Samir Genaim (2019): Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets. In: Bor-Yuh Evan Chang: Proceedings of the 26th International Symposium on Static Analysis, SAS'19, Lecture Notes in Computer Science 11822. Springer, pp. 459–480, doi:10.1007/978-3-030-32304-2_22.
  5. Amir M. Ben-Amram & Samir Genaim (2013): On the Linear Ranking Problem for Integer Linear-Constraint Loops. In: Principles of programming languages, POPL'13. ACM, pp. 51–62, doi:10.1145/2480359.2429078.
  6. Amir M. Ben-Amram & Samir Genaim (2014): Ranking Functions for Linear-Constraint Loops. Journal of the ACM 61(4), pp. 26:1–26:55, doi:10.1145/2629488.
  7. Amir M. Ben-Amram & Samir Genaim (2015): Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. In: Daniel Kroening & Corina S. Păsăreanu: Computer Aided Verification, CAV'14, LNCS 9207. Springer, pp. 304–321, doi:10.1007/978-3-319-21668-3_18.
  8. Amir M. Ben-Amram & Samir Genaim (2017): On Multiphase-Linear Ranking Functions. In: Rupak Majumdar & Viktor Kuncak: Computer Aided Verification, CAV'17, LNCS 10427. Springer, pp. 601–620, doi:10.1007/978-3-319-63390-9_32.
  9. Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell & Albert Rubio (2017): Proving Termination Through Conditional Termination. In: Axel Legay & Tiziana Margaria: Tools and Algorithms for the Construction and Analysis of Systems, TACAS'17, LNCS 10205, pp. 99–117, doi:10.1007/978-3-662-54577-5_6.
  10. Aaron R. Bradley, Zohar Manna & Henny B. Sipma (2005): Linear Ranking with Reachability. In: Kousha Etessami & Sriram K. Rajamani: Computer Aided Verification, CAV'05, LNCS 3576. Springer, pp. 491–504, doi:10.1007/11513988_48.
  11. Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs & Jürgen Giesl (2016): Analyzing Runtime and Size Complexity of Integer Programs. ACM Transactions on Programming Languages and Systems, TOPLAS'16 38(4), pp. 13:1–13:50. Available at https://doi.org/10.1145/2866575.
  12. Maurice Bruynooghe, Michael Codish, John P. Gallagher, Samir Genaim & Wim Vanhoof (2007): Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems, TOPLAS'07 29(2), pp. 10–54. Available at https://doi.org/10.1145/1216374.1216378.
  13. Michael Colón & Henny Sipma (2001): Synthesis of Linear Ranking Functions. In: Tiziana Margaria & Wang Yi: Tools and Algorithms for the Construction and Analysis of Systems, TACAS'01, LNCS 2031. Springer, pp. 67–81, doi:10.1007/3-540-45319-9_6.
  14. Jesús J. Domenech (2021): Termination Analysis of Programs with Complex Control-Flow. Facultad de Informática, Universidad Complutense de Madrid.
  15. Jesús J. Doménech, John P. Gallagher & Samir Genaim (2019): Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis. Theory Pract. Log. Program. 19(5-6), pp. 990–1005, doi:10.1017/S1471068419000310.
  16. Paul Feautrier (1992): Some efficient solutions to the affine scheduling problem. I. One-dimensional time. International Journal of Parallel Programming 21(5), pp. 313–347. Available at https://doi.org/10.1007/BF01407835.
  17. Antonio Flores-Montoya & Reiner Hähnle (2014): Resource Analysis of Complex Programs with Cost Equations. In: Jacques Garrigue: Asian Symposium on Programming Languages and Systems, APLAS'14, LNCS 8858. Springer, pp. 275–295. Available at https://doi.org/10.1007/978-3-319-12736-1_15.
  18. John P. Gallagher (2019): Polyvariant program specialisation with property-based abstraction. In: Alexei Lisitsa & Andrei P. Nemytykh: Verification and Program Transformation, VPT'19 299. Open Publishing Association, pp. 34–48. Available at https://doi.org/10.4204/eptcs.299.6.
  19. Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski & René Thiemann (2017): Analyzing Program Termination and Complexity Automatically with AProVE. Journal of Automated Reasoning 58(1), pp. 3–31. Available at https://doi.org/10.1007/s10817-016-9388-y.
  20. Sumit Gulwani, Sagar Jain & Eric Koskinen (2009): Control-flow refinement and progress invariants for bound analysis. In: Michael Hind & Amer Diwan: Programming Language Design and Implementation, PLDI'09 44. ACM, pp. 375–385. Available at https://doi.org/10.1145/1542476.1542518.
  21. Radu Iosif, Filip Konečný & Marius Bozga (2014): Deciding Conditional Termination. Logical Methods in Computer Science 10(3), doi:10.2168/lmcs-10(3:8)2014. Available at http://doi.org/10.2168/LMCS-10(3:8)2014.
  22. Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell & Albert Rubio (2013): Proving termination of imperative programs using Max-SMT. In: Formal Methods in Computer-Aided Design, FMCAD'13. IEEE, pp. 218–225. Available at https://doi.org/10.1109/FMCAD.2013.6679413.
  23. Chin Soon Lee, Neil D. Jones & Amir M. Ben-Amram (2001): The size-change principle for program termination. In: Chris Hankin & Dave Schmidt: Principles of Programming Languages, POPL'01. ACM, pp. 81–92. Available at https://doi.org/10.1145/360204.360210.
  24. Jan Leike & Matthias Heizmann (2015): Ranking Templates for Linear Loops. Logical Methods in Computer Science 11(1), pp. 1–27, doi:10.2168/LMCS-11(1:16)2015.
  25. Yi Li, Guang Zhu & Yong Feng (2016): The L-Depth Eventual Linear Ranking Functions for Single-Path Linear Constraint Loops. In: Theoretical Aspects of Software Engineering, TASE'16. IEEE, pp. 30–37. Available at https://doi.org/10.1109/TASE.2016.8.
  26. Naomi Lindenstrauss & Yehoshua Sagiv (1997): Automatic Termination Analysis of Logic Programs. In: Lee Naish: International Conference on Logic Programming, ICLP'97. MIT Press, pp. 64–77. Available at https://ieeexplore.ieee.org/document/6279160.
  27. Stephen Magill, Ming-Hsien Tsai, Peter Lee & Yih-Kuen Tsay (2010): Automatic numeric abstractions for heap-manipulating programs. In: Manuel V. Hermenegildo & Jens Palsberg: Principles of Programming Languages, POPL'10. ACM, pp. 211–222. Available at https://doi.org/10.1145/1706299.1706326.
  28. Frédéric Mesnard & Alexander Serebrenik (2008): Recurrence with affine level mappings is P-time decidable for CLP(R). Theory and Practice of Logic Programming, TPLP'08 8(1), pp. 111–119. Available at https://doi.org/10.1017/S1471068407003122.
  29. Andreas Podelski & Andrey Rybalchenko (2004): A Complete Method for the Synthesis of Linear Ranking Functions. In: Bernhard Steffen & Giorgio Levi: Verification, Model Checking, and Abstract Interpretation, VMCAI'04, LNCS 2937. Springer, pp. 239–251, doi:10.1007/978-3-540-24622-0_20.
  30. Rahul Sharma, Isil Dillig, Thomas Dillig & Alex Aiken (2011): Simplifying Loop Invariant Generation Using Splitter Predicates. In: Ganesh Gopalakrishnan & Shaz Qadeer: Computer Aided Verification, CAV'11, LNCS 6806. Springer, pp. 703–719, doi:10.1007/s10990-006-8609-1.
  31. Kirack Sohn & Allen Van Gelder (1991): Termination Detection in Logic Programs using Argument Sizes. In: Daniel J. Rosenkrantz: Principles of Database Systems, PoDS'91. ACM Press, pp. 216–226. Available at https://doi.org/10.1145/113413.113433.
  32. Fausto Spoto, Fred Mesnard & Étienne Payet (2010): A termination analyzer for Java bytecode based on path-length. ACM Transactions on Programming Languages and Systems, TOPLAS'10 32(3). Available at https://doi.org/10.1145/1709093.1709095.
  33. Alan M. Turing (1949): Checking a Large Routine. In: Report on a Conference on High Speed Automatic Computation, June 1949. University Mathematical Laboratory, Cambridge University, pp. 67–69. Available at http://www.turingarchive.org/browse.php/B/8.
  34. Yue Yuan, Yi Li & Wenchang Shi (2021): Detecting multiphase linear ranking functions for single-path linear-constraint loops. Int. J. Softw. Tools Technol. Transf. 23(1), pp. 55–67, doi:10.1007/s10009-019-00527-1.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org