{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:21:01Z","timestamp":1778498461395,"version":"3.51.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_44","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"658-674","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation"],"prefix":"10.1007","author":[{"given":"Yu-Fang","family":"Chen","sequence":"first","affiliation":[]},{"given":"Chih-Duo","family":"Hong","sequence":"additional","affiliation":[]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"44_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-319-10936-7_6","volume-title":"Static Analysis","author":"A Chakarov","year":"2014","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 85\u2013100. Springer, Heidelberg (2014)"},{"key":"44_CR2","unstructured":"Charles, K., Hang-Chin, L.: Vandermonde determinant and Lagrange interpolation in $$\\mathbb{R}^s$$ . In: Nonlinear and Convex Analysis: Proceedings in Honor of Ky Fan, vol. 107, p. 23. CRC Press (1987)"},{"key":"44_CR3","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, 20\u201323 May 1975, pp. 134\u2013183. Springer (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"44_CR4","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":"44_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"issue":"3","key":"44_CR6","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF01890412","volume":"6","author":"C Boor De","year":"1990","unstructured":"De Boor, C., Ron, A.: On multivariate polynomial interpolation. Constructive Approximation 6(3), 287\u2013302 (1990)","journal-title":"Constructive Approximation"},{"key":"44_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"03","key":"44_CR8","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1142\/S012905410200114X","volume":"13","author":"J Hartog Den","year":"2002","unstructured":"Den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a hoare like logic. Int. J. Found. Comput. Sci. 13(03), 315\u2013340 (2002)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"44_CR9","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-hall, Englewood Cliffs (1976)"},{"issue":"2","key":"44_CR10","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. Acm Sigsam Bulletin 31(2), 2\u20139 (1997)","journal-title":"Acm Sigsam Bulletin"},{"key":"44_CR11","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-59932-3_11","volume-title":"Algorithmic Algebra and Number Theory","author":"A Dolzmann","year":"1999","unstructured":"Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. In: Matzat, B.H., Greuel, G.-M., Hiss, G. (eds.) Algorithmic Algebra and Number Theory, pp. 221\u2013247. Springer, Heidelberg (1999)"},{"key":"44_CR12","volume-title":"GNU Octave","author":"JW Eaton","year":"1997","unstructured":"Eaton, J.W., Bateman, D., Hauberg, S.: GNU Octave. Network thoery, London (1997)"},{"key":"44_CR13","series-title":"Power Systems","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-25215-0_1","volume-title":"The Common Information Model CIM","author":"M Uslar","year":"2012","unstructured":"Uslar, M., Specht, M., Rohjans, S., Trefke, J., Gonzalez, J.M.V.: Introduction. In: Uslar, M., Specht, M., Rohjans, S., Trefke, J., Gonzalez, J.M.V. (eds.) The Common Information Model CIM. POWSYS, vol. 2, pp. 3\u201348. Springer, Heidelberg (2012)"},{"issue":"1","key":"44_CR14","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19(1), 19\u201332 (1967)","journal-title":"Math. Aspects Comput. Sci."},{"key":"44_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-40196-1_17","volume-title":"Quantitative Evaluation of Systems","author":"F Gretz","year":"2013","unstructured":"Gretz, F., Katoen, J.-P., McIver, A.: Prinsys\u2014on a quest for probabilistic loop invariants. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 193\u2013208. Springer, Heidelberg (2013)"},{"key":"44_CR16","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.peva.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"key":"44_CR17","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: ACM SIGPLAN Notices, vol. 43, pp. 281\u2013292. ACM (2008)","DOI":"10.1145\/1379022.1375616"},{"key":"44_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-00768-2_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gupta","year":"2009","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 262\u2013276. Springer, Heidelberg (2009)"},{"key":"44_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-642-02658-4_48","volume-title":"Computer Aided Verification","author":"A Gupta","year":"2009","unstructured":"Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634\u2013640. Springer, Heidelberg (2009)"},{"issue":"10","key":"44_CR20","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12(10), 576\u2013580 (1969)","journal-title":"CACM"},{"key":"44_CR21","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination-preliminary report. In: IMACS International Conference on Applications of Computer Algebra. Citeseer (2004)"},{"key":"44_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J-P Katoen","year":"2010","unstructured":"Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs: In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010)"},{"issue":"3","key":"44_CR23","first-page":"328","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. JCSS 22(3), 328\u2013350 (1981)","journal-title":"JCSS"},{"key":"44_CR24","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2006","unstructured":"McIver, A., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Heidelberg (2006)"},{"key":"44_CR25","doi-asserted-by":"crossref","unstructured":"Morgan, C.: Proof rules for probabilistic loops. In: Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing. Springer Verlag. (1996)","DOI":"10.14236\/ewic\/RW1996.10"},{"issue":"2","key":"44_CR26","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1111\/j.1467-9590.2006.00335.x","volume":"116","author":"PJ Olver","year":"2006","unstructured":"Olver, P.J.: On multivariate interpolation. Stud. Appl. Math. 116(2), 201\u2013240 (2006)","journal-title":"Stud. Appl. Math."},{"issue":"1","key":"44_CR27","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/0022-314X(80)90084-0","volume":"12","author":"MO Rabin","year":"1980","unstructured":"Rabin, M.O.: Probabilistic algorithm for testing primality. J. Number Theory 12(1), 128\u2013138 (1980)","journal-title":"J. Number Theory"},{"key":"44_CR28","doi-asserted-by":"crossref","unstructured":"Saniee, K.: A simple expression for multivariate Lagrange interpolation. SIAM Undergraduate Research Online 1(1) (2008)","DOI":"10.1137\/08S010025"},{"issue":"1","key":"44_CR29","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1145\/982962.964028","volume":"39","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. ACM SIGPLAN Notices 39(1), 318\u2013329 (2004)","journal-title":"ACM SIGPLAN Notices"},{"issue":"211","key":"44_CR30","doi-asserted-by":"publisher","first-page":"1147","DOI":"10.1090\/S0025-5718-1995-1297477-5","volume":"64","author":"T Sauer","year":"1995","unstructured":"Sauer, T., Xu, Y.: On multivariate Lagrange interpolation. Math. Comput. 64(211), 1147\u20131170 (1995)","journal-title":"Math. Comput."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T03:09:30Z","timestamp":1652843370000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}