{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T20:40:50Z","timestamp":1783716050580,"version":"3.55.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319681665","type":"print"},{"value":"9783319681672","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_22","type":"book-chapter","created":{"date-parts":[[2017,9,26]],"date-time":"2017-09-26T03:50:53Z","timestamp":1506397853000},"page":"327-343","source":"Crossref","is-referenced-by-count":12,"title":["Synthesizing Invariants by Solving Solvable Loops"],"prefix":"10.1007","author":[{"given":"Steven","family":"de Oliveira","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Virgile","family":"Prevosto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"22_CR1","unstructured":"Benchmark for the invariant generation. http:\/\/steven-de-oliveira.fr\/content\/bench\/pilat_nd.pdf"},{"key":"22_CR2","unstructured":"IEEE Standard for Floating-Point Arithmetic. IEEE 754-2008"},{"key":"22_CR3","unstructured":"PILAT. https:\/\/github.com\/Stevendeo\/Pilat"},{"issue":"1","key":"22_CR4","doi-asserted-by":"crossref","first-page":"23","DOI":"10.2168\/LMCS-8(1:1)2012","volume":"8","author":"A Adj\u00e9","year":"2012","unstructured":"Adj\u00e9, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. Log. Methods Comput. Sci. 8(1), 23\u201342 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/11547662_4","volume-title":"Static Analysis","author":"R Bagnara","year":"2005","unstructured":"Bagnara, R., Rodr\u00edguez-Carbonell, E., Zaffanella, E.: Generation of basic semi-algebraic invariants using convex polyhedra. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 19\u201334. Springer, Heidelberg (2005). doi: 10.1007\/11547662_4"},{"key":"22_CR6","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI C Specification Language (2008)"},{"key":"22_CR7","volume-title":"Constrained Optimization and Lagrange Multiplier Methods","author":"DP Bertsekas","year":"2014","unstructured":"Bertsekas, D.P.: Constrained Optimization and Lagrange Multiplier Methods. Academic Press, Cambridge (2014)"},{"key":"22_CR8","first-page":"89","volume":"93","author":"D Cachera","year":"2014","unstructured":"Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: a farewell to Gr\u00f6bner bases. SCP 93, 89\u2013109 (2014)","journal-title":"SCP"},{"key":"22_CR9","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, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45069-6_39"},{"key":"22_CR10","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 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-46520-3_30","volume-title":"Automated Technology for Verification and Analysis","author":"S Oliveira","year":"2016","unstructured":"Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 479\u2013494. Springer, Cham (2016). doi: 10.1007\/978-3-319-46520-3_30"},{"key":"22_CR12","unstructured":"de Oliveira, S., Bensalem, S., Prevosto, V.: Synthesizing invariants by solving solvable loops. Technical report, CEA (2016). http:\/\/steven-de-oliveira.fr\/content\/publis\/2017_atva.pdf"},{"issue":"1","key":"22_CR13","doi-asserted-by":"crossref","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), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"22_CR14","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.scico.2013.09.016","volume":"93","author":"L Gonnord","year":"2014","unstructured":"Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Sci. Comput. Program. 93, 125\u2013153 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"22_CR15","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1145\/2578855.2535843","volume":"49","author":"B Jeannet","year":"2014","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. ACM SIGPLAN Not. 49(1), 529\u2013540 (2014)","journal-title":"ACM SIGPLAN Not."},{"issue":"2","key":"22_CR16","doi-asserted-by":"crossref","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 6(2), 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"issue":"3","key":"22_CR17","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Form. Asp. Comput. 27(3), 573\u2013609 (2015)","journal-title":"Form. Asp. Comput."},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-71070-7_22","volume-title":"Automated Reasoning","author":"L Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Aligator: a mathematica package for invariant generation (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 275\u2013282. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_22"},{"key":"22_CR19","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. 4963, pp. 249\u2013264. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_18"},{"key":"22_CR20","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. 5947, pp. 242\u2013256. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11486-1_21"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1007\/978-3-662-49498-1_22","volume-title":"Programming Languages and Systems","author":"A Min\u00e9","year":"2016","unstructured":"Min\u00e9, A., Breck, J., Reps, T.: An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 560\u2013588. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49498-1_22"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1016","DOI":"10.1007\/978-3-540-27836-8_85","volume-title":"Automata, Languages and Programming","author":"M M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: A note on Karr\u2019s algorithm. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016\u20131028. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27836-8_85"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: ACM SIGPLAN Notices, vol. 39. ACM (2004)","DOI":"10.1145\/964001.964029"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: 2012 34th International Conference on Software Engineering (ICSE), pp. 683\u2013693. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to generate disjunctive invariants. In: Proceedings of 36th International Conference on Software Engineering, pp. 608\u2013619. ACM (2014)","DOI":"10.1145\/2568225.2568275"},{"issue":"1","key":"22_CR26","doi-asserted-by":"crossref","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. 64(1), 54\u201375 (2007)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"22_CR27","doi-asserted-by":"crossref","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. J. Symb. Comput. 42(4), 443\u2013476 (2007)","journal-title":"J. Symb. Comput."},{"key":"22_CR28","unstructured":"Roux, P.: Analyse statique de syst\u00e8mes de contr\u00f4le commande: synth\u00e8se d\u2019invariants non lin\u00e9aires. Ph.D. thesis, Toulouse, ISAE (2013)"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Roux, P., Jobredeaux, R., Garoche, P.-L., F\u00e9ron, \u00c9.: A generic ellipsoid abstract domain for linear time invariant systems. In: Proceedings of 15th ACM International Conference on Hybrid Systems: Computation and Control, pp. 105\u2013114. ACM (2012)","DOI":"10.1145\/2185632.2185651"},{"key":"22_CR30","unstructured":"Stein, W., et al.: Sage: Open Source Mathematical Software. 7 December 2009 (2008)"},{"key":"22_CR31","unstructured":"Wolfram|Alpha. Polynomial invariant for the simple_filter function, http:\/\/www.wolframalpha.com\/input\/?i=(-2.14285714286*(s1*s0)%2B1.42857142857*(s0*s0))%2B1.*(s1*s1)+%3C%3D++0.87891"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,18]],"date-time":"2020-10-18T07:18:36Z","timestamp":1603005516000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}