{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:53:39Z","timestamp":1725573219579},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540254355"},{"type":"electronic","value":"9783540319870"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31987-0_8","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T13:42:00Z","timestamp":1292852520000},"page":"94-107","source":"Crossref","is-referenced-by-count":6,"title":["Summaries for While Programs with Recursion"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Podelski","sequence":"first","affiliation":[]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[]},{"given":"Silke","family":"Wagner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Proceedings of CAV 2000 (2000)","DOI":"10.1007\/3-540-44585-4_18"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proceedings of PLDI 2001 (2001)","DOI":"10.1145\/378795.378846"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: Bebop: A symbolic model checker for boolean programs. In: SPIN Workshop on Model Checking of Software (2000)","DOI":"10.1007\/10722468_7"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/3-540-48224-5_54","volume-title":"Automata, Languages and Programming","author":"M. Benedikt","year":"2001","unstructured":"Benedikt, M., Godefroid, P., Reps, T.: Model checking of unrestrcited hierachical state machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, p. 652. Springer, Heidelberg (2001)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Proceedings of POPL 2003 (2003)","DOI":"10.1145\/604131.604137"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 67. Springer, Heidelberg (2001)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977 (1977)","DOI":"10.1145\/512950.512973"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of POPL 1979 (1979)","DOI":"10.1145\/567752.567778"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-27864-1_19","volume-title":"Static Analysis","author":"B. Jeannet","year":"2004","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 246\u2013264. Springer, Heidelberg (2004)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - Cade-13","author":"D.A. McAllester","year":"1996","unstructured":"McAllester, D.A., Arkoudas, K.: Walther recursion. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104. Springer, Heidelberg (1996)"},{"key":"8_CR13","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":"8_CR14","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of LICS 2004 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Proceedings of POPL 2005 (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"8_CR16","unstructured":"Podelski, A., Schaefer, I., Wagner, S.: Summaries for While Programs with Recursion. Technical Report MPI-I-2004-1-007, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany (2004)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rajamani, S., Rehof, J.: Summarizing procedures in concurrent programs. In: Proceedings of POPL 2004 (2004)","DOI":"10.1145\/964001.964022"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Ramsey, F.P.: On a problem of formal logic. In: Proceedings London Math. Soc (1930)","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Reps, T., Sagiv, M., Horwitz, S.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL 1995 (1995)","DOI":"10.1145\/199448.199462"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_11","volume-title":"Static Analysis","author":"T.W. Reps","year":"2003","unstructured":"Reps, T.W., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694. Springer, Heidelberg (2003)"},{"key":"8_CR21","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Program Flow Analysis: Theory and Applications (1981)"},{"key":"8_CR22","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":"8_CR23","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of LICS 1986 (1986)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31987-0_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:33:23Z","timestamp":1605742403000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31987-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540254355","9783540319870"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31987-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}