{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:47Z","timestamp":1751660507600},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642331244"},{"type":"electronic","value":"9783642331251"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33125-1_7","type":"book-chapter","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T06:47:24Z","timestamp":1346222844000},"page":"58-74","source":"Crossref","is-referenced-by-count":11,"title":["Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gr\u00f6bner Bases"],"prefix":"10.1007","author":[{"given":"David","family":"Cachera","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Jobin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florent","family":"Kirchner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-642-15640-3_17","volume-title":"Trustworthly Global Computing","author":"F. Besson","year":"2010","unstructured":"Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Certified Result Checking for Polyhedral Analysis of Bytecode Programs. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010, LNCS, vol.\u00a06084, pp. 253\u2013267. Springer, Heidelberg (2010)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Fast inference of polynomial invariants for imperative programs. Research Report RR-7627, INRIA (2011)","DOI":"10.1007\/978-3-642-33125-1_7"},{"key":"7_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":"M. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"7_CR4","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: POPL, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, varieties, and algorithms, 3rd edn. Undergraduate Texts in Mathematics. Springer (2007)","DOI":"10.1007\/978-0-387-35651-8"},{"key":"7_CR7","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-11486-1_21","volume-title":"Perspectives of Systems Informatics","author":"L. Kov\u00e1cs","year":"2010","unstructured":"Kov\u00e1cs, L.: A Complete Invariant Generation Approach for P-solvable Loops. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol.\u00a05947, pp. 242\u2013256. Springer, Heidelberg (2010)"},{"key":"7_CR10","unstructured":"Manna, Z.: Mathematical Theory of Computation. McGraw-Hill (1974)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-45789-5_4","volume-title":"Static Analysis","author":"M. M\u00fcller-Olm","year":"2002","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Polynomial Constants Are Decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 4\u201319. Springer, Heidelberg (2002)"},{"issue":"5","key":"7_CR12","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. Information Processing Letters\u00a091(5), 233\u2013244 (2004)","journal-title":"Information Processing Letters"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11672142_3","volume-title":"STACS 2006","author":"M. M\u00fcller-Olm","year":"2006","unstructured":"M\u00fcller-Olm, M., Petter, M., Seidl, H.: Interprocedurally Analyzing Polynomial Identities. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol.\u00a03884, pp. 50\u201367. Springer, Heidelberg (2006)"},{"key":"7_CR14","unstructured":"Petter, M.: Berechnung von polynomiellen Invarianten. Master\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2004)"},{"key":"7_CR15","unstructured":"Petter, M., Seidl, H.: Inferring polynomial program invariants with Polyinvar. Short paper, NSAD (2005)"},{"key":"7_CR16","unstructured":"Rodr\u00edguez-Carbonell, E.: Some programs that need polynomial invariants in order to be verified, \n                    \n                      http:\/\/www.lsi.upc.edu\/~erodri\/webpage\/polynomial_invariants\/list.html"},{"issue":"1","key":"7_CR17","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. Science of Computer Programming\u00a064(1), 54\u201375 (2007)","journal-title":"Science of Computer Programming"},{"issue":"4","key":"7_CR18","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E. Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation\u00a042(4), 443\u2013476 (2007)","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR19","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. ACM Press (2004)","DOI":"10.1145\/982962.964028"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33125-1_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:56:18Z","timestamp":1620129378000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33125-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642331244","9783642331251"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33125-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}