{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:39:07Z","timestamp":1743014347569,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319259413"},{"type":"electronic","value":"9783319259420"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25942-0_16","type":"book-chapter","created":{"date-parts":[[2015,10,16]],"date-time":"2015-10-16T05:32:14Z","timestamp":1444973534000},"page":"243-257","source":"Crossref","is-referenced-by-count":2,"title":["Generating Specifications for Recursive Methods by Abstracting Program States"],"prefix":"10.1007","author":[{"given":"Nathan","family":"Wasser","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"key":"16_CR1","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: 4th Symposium on Principles of Programming Languages (POPL), pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer aided verification, pp. 154\u2013169. Springer (2000)","DOI":"10.1007\/10722167_15"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2004, pp. 318\u2013329. ACM (2004)","DOI":"10.1145\/982962.964028"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-15025-8_15","volume-title":"Fields of Logic and Computation","author":"CA Furia","year":"2010","unstructured":"Furia, C.A., Meyer, B.: Inferring loop invariants using postconditions. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 277\u2013300. Springer, Heidelberg (2010)"},{"issue":"1\u20133","key":"16_CR6","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 260. Springer, Heidelberg (2001)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2002, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"La Torre, S., Parthasarathy, M., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2009, pp. 211\u2013222. ACM (2009)","DOI":"10.1145\/1542476.1542500"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-04167-9_13","volume-title":"Formal Methods for Components and Objects","author":"R Bubel","year":"2009","unstructured":"Bubel, R., H\u00e4hnle, R., Wei\u00df, B.: Abstract interpretation of symbolic execution with explicit state updates. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 247\u2013277. Springer, Heidelberg (2009)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/11916277_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2006","unstructured":"R\u00fcmmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 422\u2013436. Springer, Heidelberg (2006)"},{"key":"16_CR13","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S., Jones, N., (eds.) Program Flow Analysis: Theory and Applications. pp.189\u2013233, Prentice-Hall (1981)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, pp. 113\u2013130. Springer (2000)","DOI":"10.1007\/10722468_7"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/978-3-319-10936-7_8","volume-title":"Static Analysis","author":"Y-F Chen","year":"2014","unstructured":"Chen, Y.-F., Hsieh, C., Tsai, M.-H., Wang, B.-Y., Wang, F.: Verifying recursive programs using intraprocedural analyzers. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 118\u2013133. Springer, Heidelberg (2014)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., M. Leino, K.R.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, p. 500. Springer, Heidelberg (2001)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using boolean satisfiability. ACM Trans. Program. Lang. Syst. 29(3), May 2007","DOI":"10.1145\/1232420.1232423"},{"key":"16_CR18","unstructured":"Wasser, N., Bubel, R., H\u00e4hnle, R.: Array abstraction with symbolic pivots. Technical report, Department of Computer Science, Technische Universit\u00e4t Darmstadt, Germany August 2015. URL: \n                      https:\/\/www.se.tu-darmstadt.de\/fileadmin\/user_upload\/Group_SE\/Publications\/ALBIA\/TR_Symbolic_Pivots.pdf"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-10181-1_4","volume-title":"Integrated Formal Methods","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., K\u00e4sdorf, S., H\u00e4hnle, R., Bubel, R.: An interactive verification tool meets an IDE. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 55\u201370. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering: Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25942-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T02:53:14Z","timestamp":1559271194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25942-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259413","9783319259420"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25942-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}