{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:10:16Z","timestamp":1775790616589,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"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_26","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"400-416","source":"Crossref","is-referenced-by-count":28,"title":["Finding Polynomial Loop Invariants for Probabilistic Programs"],"prefix":"10.1007","author":[{"given":"Yijun","family":"Feng","sequence":"first","affiliation":[]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6636-3301","authenticated-orcid":false,"given":"David N.","family":"Jansen","sequence":"additional","affiliation":[]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. arXiv preprint arXiv:1605.02765 (2016)","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"26_CR2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611972290","volume-title":"Semidefinite Optimization and Convex Algebraic Geometry","year":"2012","unstructured":"Blekherman, G., Parrilo, P.A., Thomas, R.R. (eds.): Semidefinite Optimization and Convex Algebraic Geometry. SIAM, Philadelphia (2012). doi: 10.1137\/1.9781611972290"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_34"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) SAS 2014. LNCS, vol. 8723, pp. 85\u2013100. Springer, Cham (2014). doi: 10.1007\/978-3-319-10936-7_6"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). doi: 10.1007\/978-3-319-41528-4_1"},{"key":"26_CR6","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Bodik, R., Majumdar, R. (eds.) POPL\u201916, pp. 327\u2013342. ACM, New York (2016). doi: 10.1145\/2837614.2837639","DOI":"10.1145\/2837614.2837639"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-319-21690-4_44","volume-title":"Computer Aided Verification","author":"Y-F Chen","year":"2015","unstructured":"Chen, Y.-F., Hong, C.-D., Wang, B.-Y., Zhang, L.: Counterexample-guided polynomial loop invariant generation by lagrange interpolation. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 658\u2013674. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_44"},{"key":"26_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":"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, Berlin (2003). doi: 10.1007\/978-3-540-45069-6_39"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-39799-8_25","volume-title":"Computer Aided Verification","author":"L Dai","year":"2013","unstructured":"Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 364\u2013380. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_25"},{"key":"26_CR10","volume-title":"A Discipline of Programming","author":"E Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming, vol. 4. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"26_CR11","volume-title":"An Introduction to Probability Theory and Its Applications","author":"W Feller","year":"1968","unstructured":"Feller, W.: An Introduction to Probability Theory and Its Applications, vol. 1. Wiley, Hoboken (1968)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding polynomial loop invariants for probabilistic programs. arXiv:1707.02690 (2017)","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"26_CR13","doi-asserted-by":"publisher","unstructured":"Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL 2015, Principles of Programming Languages, pp. 489\u2013501. ACM, New York (2015). doi: 10.1145\/2775051.2677001","DOI":"10.1145\/2775051.2677001"},{"key":"26_CR14","doi-asserted-by":"publisher","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Dwyer, M.B., Herbsleb, J. (eds.) Future of Software Engineering (FOSE 2014), pp. 167\u2013181. ACM, New York (2014). doi: 10.1145\/2593882.2593900","DOI":"10.1145\/2593882.2593900"},{"key":"26_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). doi: 10.1007\/978-3-642-40196-1_17"},{"key":"26_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. Perf. Eval. 73, 110\u2013132 (2014). doi: 10.1016\/j.peva.2013.11.004","journal-title":"Perf. Eval."},{"key":"26_CR17","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.jsc.2015.02.007","volume":"72","author":"J Han","year":"2016","unstructured":"Han, J., Jin, Z., Xia, B.: Proving inequalities and solving global optimization problems via simplified CAD projection. J. Symb. Comput. 72, 206\u2013230 (2016). doi: 10.1016\/j.jsc.2015.02.007","journal-title":"J. Symb. Comput."},{"issue":"10","key":"26_CR18","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. Commun. ACM 12(10), 576\u2013580 (1969). doi: 10.1145\/363235.363259","journal-title":"Commun. ACM"},{"issue":"1","key":"26_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jsc.2011.08.002","volume":"47","author":"EL Kaltofen","year":"2012","unstructured":"Kaltofen, E.L., Li, B., Yang, Z., Zhi, L.: Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. J. Symb. Comput. 47(1), 1\u201315 (2012). doi: 10.1016\/j.jsc.2011.08.002","journal-title":"J. Symb. Comput."},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-662-48057-1_24","volume-title":"Mathematical Foundations of Computer Science 2015","author":"BL Kaminski","year":"2015","unstructured":"Kaminski, B.L., Katoen, J.-P.: On the hardness of almost\u2013sure termination. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 307\u2013318. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48057-1_24"},{"key":"26_CR21","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, Berlin (2010). doi: 10.1007\/978-3-642-15769-1_24"},{"key":"26_CR22","doi-asserted-by":"publisher","unstructured":"L\u00f6fberg, J.: YALMIP: a toolbox for modeling and optimization in MATLAB. In: 2004 IEEE International Symposium on Computer Aided Control Systems Design (CACSD), pp. 284\u2013289. IEEE, Piscataway (2004). doi: 10.1109\/CACSD.2004.1393890","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"26_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/b138392","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, New York (2005). doi: 10.1007\/b138392"},{"issue":"3","key":"26_CR24","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Progr. Lang. Syst. 18(3), 325\u2013353 (1996). doi: 10.1145\/229542.229547","journal-title":"ACM Trans. Progr. Lang. Syst."},{"issue":"2","key":"26_CR25","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. Ser. B 96(2), 293\u2013320 (2003). doi: 10.1007\/s10107-003-0387-5","journal-title":"Math. Program. Ser. B"},{"issue":"2","key":"26_CR26","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.tcs.2008.09.025","volume":"409","author":"H Peyrl","year":"2008","unstructured":"Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theoret. Comput. Sci. 409(2), 269\u2013281 (2008). doi: 10.1016\/j.tcs.2008.09.025","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"26_CR27","doi-asserted-by":"crossref","first-page":"969","DOI":"10.1512\/iumj.1993.42.42045","volume":"42","author":"M Putinar","year":"1993","unstructured":"Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. J. 42(3), 969\u2013984 (1993)","journal-title":"Indiana Univ. Math. J."},{"issue":"4","key":"26_CR28","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. J. Symb. Comput. 42(4), 443\u2013476 (2007). doi: 10.1016\/j.jsc.2007.01.002","journal-title":"J. Symb. Comput."},{"issue":"2","key":"26_CR29","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BF01362149","volume":"207","author":"G Stengle","year":"1974","unstructured":"Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87\u201397 (1974). doi: 10.1007\/BF01362149","journal-title":"Math. Ann."},{"issue":"1\u20134","key":"26_CR30","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1080\/10556789908805766","volume":"11","author":"JF Sturm","year":"1999","unstructured":"Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim. Methods Softw. 11(1\u20134), 625\u2013653 (1999). doi: 10.1080\/10556789908805766","journal-title":"Optim. Methods Softw."}],"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_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T19:38:31Z","timestamp":1570131511000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}