References

  1. 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.
  2. Roberto Bagnara, Fred Mesnard, Andrea Pescetti & Enea Zaffanella (2012): A new look at the automatic synthesis of linear ranking functions. Inf. Comput. 215, pp. 47–67, doi:10.1016/j.ic.2012.03.003.
  3. Amir M. Ben-Amram & Samir Genaim (2014): Ranking Functions for Linear-Constraint Loops. Journal of the ACM. Accepted.
  4. Amir M. Ben-Amram, Samir Genaim & Abu Naser Masud (2012): On the Termination of Integer Loops. ACM Trans. Program. Lang. Syst. 34(4), pp. 16:1–16:24, doi:10.1145/2400676.2400679.
  5. Marius Bozga, Radu Iosif & Filip Konecný (2014): Deciding Conditional Termination. Technical Report. Available at http://arxiv.org/abs/1302.2762.
  6. Aaron Bradley, Zohar Manna & Henny Sipma (2005): Linear Ranking with Reachability. In: Kousha Etessami & Sriram Rajamani: Computer Aided Verification, Lecture Notes in Computer Science 3576. Springer Berlin / Heidelberg, pp. 247–250, doi:10.1007/11513988_48.
  7. Aaron R. Bradley, Zohar Manna & Henny B. Sipma (2005): The Polyranking Principle. In: Luís Caires, Giuseppe F. Italiano, Luís Monteiro, Catuscia Palamidessi & Moti Yung: Proc. 32nd International Colloquium on , Languages and Programming, Lecture Notes in Computer Science 3580. Springer Verlag, pp. 1349–1361, doi:10.1007/11523468_109.
  8. Marc Brockschmidt, Byron Cook & Carsten Fuhs (2013): Better Termination Proving through Cooperation. In: Natasha Sharygina & Helmut Veith: Computer Aided Verification, CAV 2013, Lecture Notes in Computer Science 8044. Springer, pp. 413–429, doi:10.1007/978-3-642-39799-8_28.
  9. Michael Colón & Henny Sipma (2001): Synthesis of Linear Ranking Functions. In: 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science 2031. Springer, pp. 67–81, doi:10.1007/3-540-45319-9_6.
  10. Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko & Mooly Sagiv (2008): Proving conditional termination. In: Computer Aided Verification, CAV'08, Lecture Notes in Computer Science 5123. Springer, pp. 328–340, doi:10.1007/978-3-540-70545-1_32.
  11. Byron Cook, Andreas Podelski & Andrey Rybalchenko (2006): Termination proofs for systems code. In: Michael I. Schwartzbach & Thomas Ball: Programming Language Design and Implementation, PLDI'06. ACM, pp. 415–426, doi:10.1145/1133981.1134029.
  12. Byron Cook, Abigail See & Florian Zuleger (2013): Ramsey vs. Lexicographic Termination Proving. In: Nir Piterman & Scott A. Smolka: Tools and Algorithms for the Construction and Analysis of Systems,TACAS 2013, Lecture Notes in Computer Science 7795. Springer, pp. 47–61, doi:10.1007/978-3-642-36742-7_4.
  13. Patrick Cousot & Nicholas Halbwachs (1978): Automatic Discovery of Linear Restraints Among Variables of a Program. In: Conference Record of the Fifth annual ACM Symposium on Principles of Programming Languages. ACM. ACM, pp. 84–96, doi:10.1145/512760.512770.
  14. Stéphane Demri (2011): Decidable Problems for Counter Systems. Available at http://www.lsv.ens-cachan.fr/~demri/esslli2010-lecture-notes.pdf. Revised lecture notes from a course at ESSLLI 2010, Copenhagen.
  15. Javier Esparza (1998): Decidability and Complexity of Petri Net Problems—An Introduction. In: Wolfgang Reisig & Grzegorz Rozenberg: Lectures on Petri Nets, Vol. I: Basic Models, LNCS 1491. Springer-Verlag (New York), Dagstuhl, Germany, pp. 374–428, doi:10.1007/3-540-65306-6_20.
  16. Javier Esparza & Mogens Nielsen (1994): Decidability Issues for Petri Nets. Technical Report RS-94-8. BRICS, Department of Computer Science, University of Aarhus.
  17. Michel H. T. Hack (1979). In: Decidability questions for Petri Nets. MIT.
  18. William R Harris, Akash Lal, Aditya V Nori & Sriram K Rajamani (2011): Alternation for termination. In: Static Analysis Symposium, SAS 2011, LNCS 6337. Springer, pp. 304–319, doi:10.1007/978-3-642-15769-1_19.
  19. Matthias Heizmann, Jochen Hoenicke, Jan Leike & Andreas Podelski (2013): Linear Ranking for Linear Lasso Programs. In: Dang Hung & Mizuhito Ogawa: Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 8172. Springer International Publishing, pp. 365–380, doi:10.1007/978-3-319-02444-8_26.
  20. Neil D. Jones (1997). In: Computability and Complexity From a Programming Perspective, Foundations of Computing Series. MIT Press.
  21. Richard M Karp & Raymond E Miller (1969): Parallel program schemata. Journal of Computer and system Sciences 3(2), pp. 147–195, doi:10.1016/S0022-0000(69)80011-5.
  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 2013. IEEE, pp. 218–225, doi:10.1109/FMCAD.2013.6679413.
  23. Jérôme Leroux (2011): Vector Addition System Reachability Problem: A Short Self-contained Proof. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11. ACM, New York, NY, USA, pp. 307–316, doi:10.1145/1926385.1926421.
  24. Richard J. Lipton (1976): The Reachability Problem Requires Exponential Space. Technical Report 63. Yale University.
  25. Frédéric Mesnard & Alexander Serebrenik (2008): Recurrence with affine level mappings is P-time decidable for CLP(R). TPLP 8(1), pp. 111–119, doi:10.1017/S1471068407003122.
  26. Joël Ouaknine & James Worrell (2014): Positivity problems for low-order linear recurrence sequences. In: Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '14. SIAM, doi:10.1137/1.9781611973402.27.
  27. 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.
  28. Andreas Podelski & Andrey Rybalchenko (2007): ARMC: the logical choice for software model checking with abstraction refinement. In: Practical Aspects of Declarative Languages, LNCS 4354. Springer, pp. 245–259, doi:10.1007/978-3-540-69611-7_16.
  29. Kirack Sohn & Allen Van Gelder (1991): Termination detection in logic programs using argument sizes (extended abstract). In: Proceedings of the Tenth ACM SIGACT-SIGMOD-SOGART Symposium on Principles of Database Systems (PODS), May 1991, Denver, Colorado. ACM Press, pp. 216–226, doi:10.1145/113413.113433.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org