{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T15:40:08Z","timestamp":1751816408462,"version":"3.41.0"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999326"},{"type":"electronic","value":"9783319999333"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99933-3_5","type":"book-chapter","created":{"date-parts":[[2018,8,25]],"date-time":"2018-08-25T12:33:39Z","timestamp":1535200419000},"page":"69-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Robust Non-termination Analysis of Numerical Software"],"prefix":"10.1007","author":[{"given":"Bai","family":"Xue","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yangjia","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiuye","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,26]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-31424-7_19","volume-title":"Computer Aided Verification","author":"MF Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Emmi, M., Lal, A.: Detecting fair non-termination in multithreaded programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 210\u2013226. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_19"},{"key":"5_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4606-6","volume-title":"Set-Theoretic Methods in Control","author":"F Blanchini","year":"2008","unstructured":"Blanchini, F., Miani, S.: Set-Theoretic Methods in Control. Springer, Boston (2008). https:\/\/doi.org\/10.1007\/978-0-8176-4606-6"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-662-54577-5_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Borralleras","year":"2017","unstructured":"Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination through conditional termination. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 99\u2013117. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_6"},{"key":"5_CR4","volume-title":"General Topology: Chapters 1\u20134","author":"N Bourbaki","year":"2013","unstructured":"Bourbaki, N.: General Topology: Chapters 1\u20134, vol. 18. Springer, Heidelberg (2013)"},{"key":"5_CR5","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611970777","volume-title":"Linear Matrix Inequalities in System and Control Theory","author":"S Boyd","year":"1994","unstructured":"Boyd, S., El Ghaoui, L., Feron, E., Balakrishnan, V.: Linear Matrix Inequalities in System and Control Theory. SIAM, Philadelphia (1994)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-31762-0_9","volume-title":"Formal Verification of Object-Oriented Software","author":"M Brockschmidt","year":"2012","unstructured":"Brockschmidt, M., Str\u00f6der, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 123\u2013141. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31762-0_9"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-54862-8_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H-Y Chen","year":"2014","unstructured":"Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O\u2019Hearn, P.: Proving nontermination via safety. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 156\u2013171. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_11"},{"key":"5_CR8","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). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_44"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Cook, B., Fuhs, C., Nimkar, K., O\u2019Hearn, P.: Disproving termination with overapproximation. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, pp. 67\u201374. FMCAD Inc. (2014)","DOI":"10.1109\/FMCAD.2014.6987597"},{"issue":"5","key":"5_CR10","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88\u201398 (2011)","journal-title":"Commun. ACM"},{"key":"5_CR11","unstructured":"Cousot, P., Cousot, R.: A gentle introduction to formal verification of computer systems by abstract interpretation (2010)"},{"key":"5_CR12","first-page":"77","volume":"44","author":"SOR Fedkiw","year":"2002","unstructured":"Fedkiw, S.O.R., Osher, S.: Level set methods and dynamic implicit surfaces. Surfaces 44, 77 (2002)","journal-title":"Surfaces"},{"issue":"19\u201332","key":"5_CR13","first-page":"1","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19(19\u201332), 1 (1967)","journal-title":"Math. Aspects Comput. Sci."},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-08587-6_13","volume-title":"Automated Reasoning","author":"J Giesl","year":"2014","unstructured":"Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184\u2013191. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_13"},{"issue":"8","key":"5_CR15","doi-asserted-by":"publisher","first-page":"2291","DOI":"10.3934\/dcdsb.2015.20.2291","volume":"20","author":"P Giesl","year":"2015","unstructured":"Giesl, P., Hafstein, S.: Review on computational methods for Lyapunov functions. Discrete Contin. Dyn. Syst.-Ser. B 20(8), 2291\u20132331 (2015)","journal-title":"Discrete Contin. Dyn. Syst.-Ser. B"},{"issue":"1","key":"5_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/1328897.1328459","volume":"43","author":"A Gupta","year":"2008","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. ACM Sigplan Not. 43(1), 147\u2013158 (2008)","journal-title":"ACM Sigplan Not."},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-15769-1_19","volume-title":"Static Analysis","author":"WR Harris","year":"2010","unstructured":"Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 304\u2013319. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_19"},{"issue":"10","key":"5_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)","journal-title":"Commun. ACM"},{"key":"5_CR19","unstructured":"Jarvis-Wloszek, Z.W.: Lyapunov based analysis and controller synthesis for polynomial systems using sum-of-squares optimization. Ph.D. thesis, University of California, Berkeley (2003)"},{"key":"5_CR20","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2006)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Kouramas, K.I., Rakovic, S.V., Kerrigan, E.C., Allwright, J., Mayne, D.Q.: On the minimal robust positively invariant set for linear difference inclusions. In: 44th IEEE Conference on Decision and Control, 2005 and 2005 European Control Conference, CDC-ECC 2005, pp. 2296\u20132301. IEEE (2005)","DOI":"10.1109\/CDC.2005.1582504"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-319-21668-3_17","volume-title":"Computer Aided Verification","author":"T Kuwahara","year":"2015","unstructured":"Kuwahara, T., Sato, R., Unno, H., Kobayashi, N.: Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 287\u2013303. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_17"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1007\/978-3-319-08867-9_52","volume-title":"Computer Aided Verification","author":"D Larraz","year":"2014","unstructured":"Larraz, D., Nimkar, K., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving non-termination using max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779\u2013796. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_52"},{"issue":"2","key":"5_CR24","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10107-014-0838-1","volume":"151","author":"JB Lasserre","year":"2015","unstructured":"Lasserre, J.B.: Tractable approximations of sets defined with quantifiers. Math. Programm. 151(2), 507\u2013527 (2015)","journal-title":"Math. Programm."},{"key":"5_CR25","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.tcs.2017.03.036","volume":"681","author":"Y Li","year":"2017","unstructured":"Li, Y.: Witness to non-termination of linear programs. Theor. Comput. Sci. 681, 75\u2013100 (2017)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"5_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-013-4961-z","volume":"57","author":"W Lin","year":"2014","unstructured":"Lin, W., Wu, M., Yang, Z., Zeng, Z.: Exact safety verification of hybrid systems using sums-of-squares representation. Sci. China Inf. Sci. 57(5), 1\u201313 (2014)","journal-title":"Sci. China Inf. Sci."},{"issue":"6","key":"5_CR27","doi-asserted-by":"publisher","first-page":"1286","DOI":"10.1007\/s11424-014-2145-6","volume":"27","author":"J Liu","year":"2014","unstructured":"Liu, J., Xu, M., Zhan, N., Zhao, H.: Discovering non-terminating inputs for multi-path polynomial programs. J. Syst. Sci. Complex. 27(6), 1286\u20131304 (2014)","journal-title":"J. Syst. Sci. Complex."},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Proceedings of the Ninth ACM International Conference on Embedded Software, pp. 97\u2013106. ACM (2011)","DOI":"10.1145\/2038642.2038659"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Lofberg, J.: YALMIP: a toolbox for modeling and optimization in MATLAB. In: 2004 IEEE International Symposium on Computer Aided Control Systems Design, pp. 284\u2013289. IEEE (2004)","DOI":"10.1109\/CACSD.2004.1393890"},{"issue":"15","key":"5_CR30","doi-asserted-by":"publisher","first-page":"2781","DOI":"10.1080\/00207721.2013.879232","volume":"46","author":"CK Luk","year":"2015","unstructured":"Luk, C.K., Chesi, G.: On the estimation of the domain of attraction for discrete-time switched and hybrid nonlinear systems. Int. J. Syst. Sci. 46(15), 2781\u20132787 (2015)","journal-title":"Int. J. Syst. Sci."},{"key":"5_CR31","unstructured":"Magron, V., Garoche, P.-L., Henrion, D., Thirioux, X.: Semidefinite approximations of reachable sets for discrete-time polynomial systems. arXiv preprint arXiv:1703.05085 (2017)"},{"issue":"7","key":"5_CR32","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1109\/TAC.2005.851439","volume":"50","author":"IM Mitchell","year":"2005","unstructured":"Mitchell, I.M., Bayen, A.M., Tomlin, C.J.: A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control 50(7), 947\u2013957 (2005)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR33","unstructured":"Mosek, A.: The MOSEK optimization toolbox for MATLAB manual. Version 7.1 (Revision 28), p. 17 (2015)"},{"issue":"4","key":"5_CR34","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/BF01966091","volume":"6","author":"P Naur","year":"1966","unstructured":"Naur, P.: Proof of algorithms by general snapshots. BIT Numer. Math. 6(4), 310\u2013316 (1966)","journal-title":"BIT Numer. Math."},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-02959-2_35","volume-title":"Automated Deduction \u2013 CADE-22","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D., R\u00fcmmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485\u2013501. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_35"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32"},{"issue":"8","key":"5_CR37","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transa. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Transa. Autom. Control"},{"issue":"3","key":"5_CR38","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1109\/TAC.2005.843854","volume":"50","author":"SV Rakovic","year":"2005","unstructured":"Rakovic, S.V., Kerrigan, E.C., Kouramas, K.I., Mayne, D.Q.: Invariant approximations of the minimal robust positively invariant set. IEEE Trans. Autom. Control 50(3), 406\u2013410 (2005)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR39","unstructured":"Rebiha, R., Matringe, N., Moura, A.V.: Generating asymptotically non-terminating initial values for linear programs. arXiv preprint arXiv:1407.4556 (2014)"},{"issue":"3","key":"5_CR40","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1109\/TAC.2013.2241472","volume":"58","author":"M Roozbehani","year":"2013","unstructured":"Roozbehani, M., Megretski, A., Feron, E.: Optimization of Lyapunov invariants in verification of software systems. IEEE Trans. Autom. Control 58(3), 696\u2013711 (2013)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-662-53413-7_21","volume-title":"Static Analysis","author":"P Roux","year":"2016","unstructured":"Roux, P., Voronin, Y.-L., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 424\u2013446. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_21"},{"issue":"1","key":"5_CR42","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 Not. 39(1), 318\u2013329 (2004)","journal-title":"ACM SIGPLAN Not."},{"issue":"4","key":"5_CR43","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1016\/j.sysconle.2012.01.004","volume":"61","author":"MAB Sassi","year":"2012","unstructured":"Sassi, M.A.B., Girard, A.: Controller synthesis for robust invariance of polynomial dynamical systems using linear programming. Syst. Control Lett. 61(4), 506\u2013512 (2012)","journal-title":"Syst. Control Lett."},{"key":"5_CR44","doi-asserted-by":"crossref","unstructured":"Sassi, M.A.B., Girard, A., Sankaranarayanan, S.: Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: 2014 IEEE 53rd Annual Conference on Decision and Control (CDC), pp. 6348\u20136353. IEEE (2014)","DOI":"10.1109\/CDC.2014.7040384"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Schaich, R.M., Cannon, M.: Robust positively invariant sets for state dependent and scaled disturbances. In: 2015 IEEE 54th Annual Conference on Decision and Control (CDC), pp. 7560\u20137565. IEEE (2015)","DOI":"10.1109\/CDC.2015.7403414"},{"key":"5_CR46","doi-asserted-by":"crossref","unstructured":"Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, pp. 329\u2013336. ACM (2011)","DOI":"10.1145\/1993886.1993935"},{"issue":"17","key":"5_CR47","doi-asserted-by":"publisher","first-page":"213","DOI":"10.3182\/20120823-5-NL-3013.00032","volume":"45","author":"F Tahir","year":"2012","unstructured":"Tahir, F., Jaimoukha, I.M.: Robust positively invariant sets for linear systems subject to model-uncertainty and disturbances. IFAC Proc. Vol. 45(17), 213\u2013217 (2012)","journal-title":"IFAC Proc. Vol."},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70\u201382. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_6"},{"issue":"10","key":"5_CR49","doi-asserted-by":"publisher","first-page":"2669","DOI":"10.1016\/j.automatica.2008.03.010","volume":"44","author":"U Topcu","year":"2008","unstructured":"Topcu, U., Packard, A., Seiler, P.: Local stability analysis using simulations and sum-of-squares programming. Automatica 44(10), 2669\u20132675 (2008)","journal-title":"Automatica"},{"issue":"1","key":"5_CR50","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1109\/TAC.2009.2033751","volume":"55","author":"U Topcu","year":"2010","unstructured":"Topcu, U., Packard, A.K., Seiler, P., Balas, G.J.: Robust region-of-attraction estimation. IEEE Trans. Autom. Control 55(1), 137\u2013142 (2010)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"12","key":"5_CR51","doi-asserted-by":"publisher","first-page":"4100","DOI":"10.1109\/TAC.2016.2541300","volume":"61","author":"P Trodden","year":"2016","unstructured":"Trodden, P.: A one-step approach to computing a polytopic robust positively invariant set. IEEE Trans. Autom. Control 61(12), 4100\u20134105 (2016)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"5_CR52","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1137\/1038003","volume":"38","author":"L Vandenberghe","year":"1996","unstructured":"Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Rev. 38(1), 49\u201395 (1996)","journal-title":"SIAM Rev."},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-79124-9_11","volume-title":"Tests and Proofs","author":"H Velroyen","year":"2008","unstructured":"Velroyen, H., R\u00fcmmer, P.: Non-termination checking for imperative programs. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 154\u2013170. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-79124-9_11"},{"issue":"2","key":"5_CR54","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s00165-009-0144-5","volume":"23","author":"B Xia","year":"2011","unstructured":"Xia, B., Yang, L., Zhan, N., Zhang, Z.: Symbolic decision procedure for termination of linear programs. Formal Aspects Comput. 23(2), 171\u2013190 (2011)","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"5_CR55","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11704-009-0074-7","volume":"4","author":"L Yang","year":"2010","unstructured":"Yang, L., Zhou, C., Zhan, N., Xia, B.: Recent advances in program verification through computer algebra. Front. Comput. Sci. China 4(1), 1\u201316 (2010)","journal-title":"Front. Comput. Sci. China"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99933-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T15:19:39Z","timestamp":1751815179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99933-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999326","9783319999333"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99933-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}