{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:28:13Z","timestamp":1707521293472},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,10,13]],"date-time":"2009-10-13T00:00:00Z","timestamp":1255392000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s10703-009-0087-8","type":"journal-article","created":{"date-parts":[[2009,10,12]],"date-time":"2009-10-12T20:37:41Z","timestamp":1255379861000},"page":"369-387","source":"Crossref","is-referenced-by-count":18,"title":["Summarization for termination: no return!"],"prefix":"10.1007","volume":"35","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,10,13]]},"reference":[{"key":"87_CR1","volume-title":"STOC","author":"R Alur","year":"2004","unstructured":"Alur R, Madhusudan P (2004) Visibly pushdown languages. In: STOC. ACM, New York"},{"key":"87_CR2","volume-title":"TACAS","author":"R Alur","year":"2004","unstructured":"Alur R, Etessami K, Madhusudan P (2004) A temporal logic of nested calls and returns. In: TACAS. Springer, Berlin"},{"key":"87_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Benedikt M, Etessami K, Godefroid P, Reps TW, Yannakakis M (2005) Analysis of recursive state machines. ACM Trans Program Lang Syst","DOI":"10.1145\/1075382.1075387"},{"key":"87_CR4","volume-title":"POPL","author":"R Alur","year":"2006","unstructured":"Alur R, Chaudhuri S, Madhusudan P (2006) A fixpoint calculus for local and global program flows. In: POPL. ACM, New York"},{"key":"87_CR5","volume-title":"SPIN","author":"T Ball","year":"2000","unstructured":"Ball T, Rajamani SK (2000) Bebop: A symbolic model checker for Boolean programs. In: SPIN. Springer, Berlin"},{"key":"87_CR6","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2001) Bebop: a path-sensitive interprocedural dataflow engine. In: PASTE","DOI":"10.1145\/379605.379690"},{"key":"87_CR7","volume-title":"CONCUR","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani A, Esparza J, Maler O (1997) Reachability analysis of pushdown automata: Application to model-checking. In: CONCUR. Springer, Berlin"},{"key":"87_CR8","volume-title":"PLDI","author":"F Bourdoncle","year":"1993","unstructured":"Bourdoncle F (1993) Abstract debugging of higher-order imperative languages. In: PLDI. ACM, New York"},{"key":"87_CR9","doi-asserted-by":"crossref","unstructured":"Bradley A, Manna Z, Sipma H (2005) Termination of polynomial programs. In: VMCAI","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"87_CR10","doi-asserted-by":"crossref","unstructured":"Col\u00f3n M, Sipma H (2002) Practical methods for proving program termination. In: CAV","DOI":"10.1007\/3-540-45657-0_36"},{"key":"87_CR11","volume-title":"PLDI","author":"B Cook","year":"2006","unstructured":"Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: PLDI. ACM, New York"},{"key":"87_CR12","volume-title":"Predicate calculus and program semantics","author":"EW Dijkstra","year":"1989","unstructured":"Dijkstra EW, Scholten CS (1989) Predicate calculus and program semantics. Springer, Berlin"},{"key":"87_CR13","volume-title":"POPL","author":"J Esparza","year":"2000","unstructured":"Esparza J, Podelski A (2000) Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: POPL. ACM, New York"},{"key":"87_CR14","volume-title":"CAV","author":"J Esparza","year":"2001","unstructured":"Esparza J, Schwoon S (2001) A bdd-based model checker for recursive programs. In: CAV. Springer, Berlin"},{"key":"87_CR15","volume-title":"CAV","author":"J Esparza","year":"2000","unstructured":"Esparza J, Hansel D, Rossmanith P, Schwoon S (2000) Efficient algorithms for model checking pushdown systems. In: CAV. Springer, Berlin"},{"key":"87_CR16","volume-title":"SAS","author":"A Gotsman","year":"2006","unstructured":"Gotsman A, Berdine J, Cook B (2006) Interprocedural shape analysis with separated heap abstractions. In: SAS. Springer, Berlin"},{"key":"87_CR17","volume-title":"POPL","author":"A Gupta","year":"2008","unstructured":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R-G (2008) Proving non-termination. In: POPL. ACM, New York"},{"key":"87_CR18","volume-title":"SAS","author":"B Jeannet","year":"2004","unstructured":"Jeannet B, Loginov A, Reps TW, Sagiv S (2004) A relational approach to interprocedural shape analysis. In: SAS. Springer, Berlin"},{"key":"87_CR19","volume-title":"POPL","author":"R Jhala","year":"2007","unstructured":"Jhala R, Majumdar R (2007) Interprocedural analysis of asynchronous programs. In: POPL. ACM, New York"},{"key":"87_CR20","volume-title":"PLDI","author":"J Kodumal","year":"2004","unstructured":"Kodumal J, Aiken A (2004) The set constraint\/CFL reachability connection in practice. In: PLDI. ACM, New York"},{"key":"87_CR21","volume-title":"CAV","author":"A Lal","year":"2006","unstructured":"Lal A, Reps TW (2006) Improving pushdown system model checking. In: CAV. ACM, New York"},{"key":"87_CR22","volume-title":"TACAS","author":"A Lal","year":"2008","unstructured":"Lal A, Touili T, Kidd N, Reps TW (2008) Interprocedural analysis of concurrent programs under a context bound. In: TACAS. Springer, Berlin"},{"key":"87_CR23","doi-asserted-by":"crossref","unstructured":"Lee CS, Jones ND, Ben-Amram AM (2001) The size-change principle for program termination. In: POPL","DOI":"10.1145\/360204.360210"},{"key":"87_CR24","volume-title":"CAV","author":"P Manolios","year":"2006","unstructured":"Manolios P, Vroon D (2006) Termination analysis with calling context graphs. In: CAV. Springer, Berlin"},{"key":"87_CR25","volume-title":"LICS","author":"A Podelski","year":"2004","unstructured":"Podelski A, Rybalchenko A (2004) Transition invariants. In: LICS. IEEE, New York"},{"key":"87_CR26","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A (2005) Transition predicate abstraction and fair termination. In: POPL","DOI":"10.1145\/1040305.1040317"},{"key":"87_CR27","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A (2007) ARMC: the logical choice for software model checking with abstraction refinement. In: PADL","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"87_CR28","volume-title":"ESOP","author":"A Podelski","year":"2005","unstructured":"Podelski A, Schaefer I, Wagner S (2005) Summaries for total correctness of recursive programs. In: ESOP. Springer, Berlin"},{"key":"87_CR29","volume-title":"POPL","author":"S Qadeer","year":"2004","unstructured":"Qadeer S, Rajamani SK, Rehof J (2004) Summarizing procedures in concurrent programs. In: POPL. ACM, New York"},{"key":"87_CR30","doi-asserted-by":"crossref","unstructured":"Reps TW, Horwitz S, Sagiv S (1995) Precise interprocedural dataflow analysis via graph reachability. In: POPL","DOI":"10.1145\/199448.199462"},{"key":"87_CR31","doi-asserted-by":"crossref","unstructured":"Reps TW, Schwoon S, Jha S, Melski D (2005) Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci Comput Program","DOI":"10.21236\/ADA449102"},{"key":"87_CR32","volume-title":"FSTTCS","author":"TW Reps","year":"2007","unstructured":"Reps TW, Lal A, Kidd N (2007) Program analysis using weighted pushdown systems. In: FSTTCS. Springer, Berlin"},{"key":"87_CR33","volume-title":"Program Flow Analysis: Theory and Application","author":"M Sharir","year":"1981","unstructured":"Sharir M, Pnueli A (1981) Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Application. Prentice Hall, Englewood Cliffs"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0087-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0087-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0087-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:51Z","timestamp":1559253951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0087-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10,13]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["87"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0087-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,10,13]]}}}