{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:33:01Z","timestamp":1742387581669},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_25","type":"book-chapter","created":{"date-parts":[[2014,1,2]],"date-time":"2014-01-02T20:08:09Z","timestamp":1388693289000},"page":"453-471","source":"Crossref","is-referenced-by-count":7,"title":["Policy Iteration-Based Conditional Termination and Ranking Functions"],"prefix":"10.1007","author":[{"given":"Damien","family":"Mass\u00e9","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-11957-6_3","volume-title":"Programming Languages and Systems","author":"A. Adj\u00e9","year":"2010","unstructured":"Adj\u00e9, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 23\u201342. Springer, Heidelberg (2010)"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, Martel (eds.) [15], pp. 117\u2013133","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Amato, G., Parton, M., Scozzari, F.: Deriving numerical abstract domains via principal component analysis. In: Cousot, Martel (eds.) [15], pp. 134\u2013150","DOI":"10.1007\/978-3-642-15769-1_9"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-28756-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozga","year":"2012","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Deciding conditional termination. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 252\u2013266. Springer, Heidelberg (2012)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-642-33125-1_28","volume-title":"Static Analysis","author":"H.Y. Chen","year":"2012","unstructured":"Chen, H.Y., Flur, S., Mukhopadhyay, S.: Termination proofs for linear simple loops. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 422\u2013438. Springer, Heidelberg (2012)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-642-19718-5_10","volume-title":"Programming Languages and Systems","author":"M.A. Col\u00f3n","year":"2011","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S.: Generalizing the template polyhedral domain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 176\u2013195. Springer, Heidelberg (2011)"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 328\u2013340. Springer, Heidelberg (2008)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-36742-7_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Cook","year":"2013","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 47\u201361. Springer, Heidelberg (2013)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/11513988_46","volume-title":"Computer Aided Verification","author":"A. Costan","year":"2005","unstructured":"Costan, A., Gaubert, S., Goubault, \u00c9., Martel, M., Putot, S.: A policy iteration algorithm for computing fixed points in static analysis of programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 462\u2013475. Springer, Heidelberg (2005)"},{"key":"25_CR11","unstructured":"Cousot, P.: M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes (in French). Th\u00e8se d\u2019\u00c9tat \u00e8s sciences math\u00e9matiques, Universit\u00e9 Joseph Fourier, Grenoble, France (March 21, 1978)"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/2103656.2103687","volume-title":"Conference Record of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"2012","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: Conference Record of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, PA, January 25-27, pp. 245\u2013258. ACM Press, New York (2012)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot (ed.) [14], pp. 1\u201324","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","year":"2005","unstructured":"Cousot, R. (ed.): VMCAI 2005. LNCS, vol.\u00a03385. Springer, Heidelberg (2005)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","year":"2010","unstructured":"Cousot, R., Martel, M. (eds.): SAS 2010. LNCS, vol.\u00a06337. Springer, Heidelberg (2010)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-32943-2_5","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"L. Dai","year":"2012","unstructured":"Dai, L., Xia, B.: Non-termination sets of simple linear loops. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol.\u00a07521, pp. 61\u201373. Springer, Heidelberg (2012)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","year":"2007","unstructured":"De Nicola, R. (ed.): ESOP 2007. LNCS, vol.\u00a04421. Springer, Heidelberg (2007)"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: De Nicola (ed.) [17], pp. 237\u2013252","DOI":"10.1007\/978-3-540-71316-6_17"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: De Nicola (ed.) [17], pp. 300\u2013315","DOI":"10.1007\/978-3-540-71316-6_21"},{"key":"25_CR20","unstructured":"Hogben, L.: Handbook of Linear Algebra, 1st edn. Discrete Mathematics and Its Applications. Chapman & Hall\/CRC (2007)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-14295-6_9","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2010","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 89\u2013103. Springer, Heidelberg (2010)"},{"key":"25_CR23","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.entcs.2012.09.008","volume":"287","author":"D. Mass\u00e9","year":"2012","unstructured":"Mass\u00e9, D.: Proving termination by policy iteration. Electr. Notes Theor. Comput. Sci.\u00a0287, 77\u201388 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275501"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot (ed.) [14], pp. 25\u201341","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-35873-9_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Seladji","year":"2013","unstructured":"Seladji, Y., Bouissou, O.: Fixpoint computation in the polyhedra abstract domain using convex and numerical analysis tools. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 149\u2013168. Springer, Heidelberg (2013)"},{"key":"25_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A. Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 70\u201382. Springer, Heidelberg (2004)"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-38856-9_5","volume-title":"Static Analysis","author":"C. Urban","year":"2013","unstructured":"Urban, C.: The abstract domain of segmented ranking functions. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 43\u201362. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T19:34:36Z","timestamp":1558812876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}