{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T14:19:05Z","timestamp":1726409945208},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642212031"},{"type":"electronic","value":"9783642212048"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21204-8_29","type":"book-chapter","created":{"date-parts":[[2011,5,28]],"date-time":"2011-05-28T05:15:25Z","timestamp":1306559725000},"page":"264-274","source":"Crossref","is-referenced-by-count":0,"title":["An Iterative Method for Generating Loop Invariants"],"prefix":"10.1007","author":[{"given":"Shikun","family":"Chen","sequence":"first","affiliation":[]},{"given":"Zhoujun","family":"Li","sequence":"additional","affiliation":[]},{"given":"Xiaoyu","family":"Song","sequence":"additional","affiliation":[]},{"given":"Mengjun","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-75221-9_4","volume-title":"Formal Methods and Hybrid Real-Time Systems","author":"Y. Chen","year":"2007","unstructured":"Chen, Y., Xia, B., Yang, L., Zhan, N.: Generating polynomial invariants with Discoverer and Qepcad. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol.\u00a04700, pp. 67\u201382. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, pp. 84\u201396 (1978)","key":"29_CR3","DOI":"10.1145\/512760.512770"},{"doi-asserted-by":"crossref","unstructured":"Rodriguez-Carbonell, D.K.E.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation, 443\u2013476 (2007)","key":"29_CR4","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","year":"2004","unstructured":"Giacobazzi, R. (ed.): SAS 2004. LNCS, vol.\u00a03148. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proc. PLDI 2008, pp. 281\u2013292 (2008)","key":"29_CR6","DOI":"10.1145\/1375581.1375616"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-78800-3_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Reasoning algebraically about p-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 249\u2013264. Springer, Heidelberg (2008)"},{"key":"29_CR8","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":"H.S. Michael","year":"2003","unstructured":"Michael, H.S., Colon, A., Sankaranarayanan, S.: Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013433. Springer, Heidelberg (2003)"},{"issue":"1","key":"29_CR9","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation\u00a019(1), 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL, pp. 330\u2013341 (2004a)","key":"29_CR10","DOI":"10.1145\/982962.964029"},{"issue":"5","key":"29_CR11","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett.\u00a091(5), 233\u2013244 (2004b)","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"29_CR12","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.scico.2006.03.003","volume":"64","author":"E. Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program.\u00a064(1), 54\u201375 (2007)","journal-title":"Sci. Comput. Program."},{"doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: POPL, pp. 318\u2013329 (2004)","key":"29_CR13","DOI":"10.1145\/982962.964028"}],"container-title":["Lecture Notes in Computer Science","Frontiers in Algorithmics and Algorithmic Aspects in Information and Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21204-8_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T08:10:17Z","timestamp":1560240617000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21204-8_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642212031","9783642212048"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21204-8_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}