{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:21:36Z","timestamp":1768004496806,"version":"3.49.0"},"publisher-location":"Cham","reference-count":66,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030309411","type":"print"},{"value":"9783030309428","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-30942-8_10","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"138-157","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Pegasus: A Framework for Sound Continuous Invariant Generation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5849-7991","authenticated-orcid":false,"given":"Andrew","family":"Sogokon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3194-9759","authenticated-orcid":false,"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7033-2463","authenticated-orcid":false,"given":"Yong Kiam","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9336-6006","authenticated-orcid":false,"given":"Katherine","family":"Cordwell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"issue":"7","key":"10_CR1","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000). \nhttps:\/\/doi.org\/10.1109\/5.871304","journal-title":"Proc. IEEE"},{"key":"10_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-2388-4","volume-title":"Dynamical Systems: Differential Equations, Maps, and Chaotic Behaviour","author":"D Arrowsmith","year":"1992","unstructured":"Arrowsmith, D., Place, C.M.: Dynamical Systems: Differential Equations, Maps, and Chaotic Behaviour, vol. 5. CRC Press, Boca Raton (1992)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-540-73595-3_26","volume-title":"Automated Deduction \u2013 CADE-21","author":"B Beckert","year":"2007","unstructured":"Beckert, B., et al.: The KeY system 1.0 (deduction component). In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 379\u2013384. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-73595-3_26"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Sassi, M.A.B., Girard, A., Sankaranarayanan, S.: Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: CDC 2014, pp. 6348\u20136353. IEEE (2014). \nhttps:\/\/doi.org\/10.1109\/CDC.2014.7040384","DOI":"10.1109\/CDC.2014.7040384"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14052-5_14"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Bohrer, B., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: VeriPhy: verified controller executables from verified cyber-physical system models. In: Foster, J.S., Grossman, D. (eds.) PLDI 2018, pp. 617\u2013630. ACM (2018). \nhttps:\/\/doi.org\/10.1145\/3192366.3192406","DOI":"10.1145\/3192366.3192406"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Chen, M., et al.: MARS: a toolchain for modelling, analysis and verification of hybrid systems. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE 2017, pp. 39\u201358. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-48628-4_3","DOI":"10.1007\/978-3-319-48628-4_3"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages 2nd GI Conference","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). \nhttps:\/\/doi.org\/10.1007\/3-540-07407-4_17"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Cox, D.A., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms. UTM 2015. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-16721-3","DOI":"10.1007\/978-3-319-16721-3"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1016\/j.jsc.2016.07.010","volume":"80","author":"L Dai","year":"2017","unstructured":"Dai, L., Gan, T., Xia, B., Zhan, N.: Barrier certificates revisited. J. Symb. Comput. 80, 62\u201386 (2017). \nhttps:\/\/doi.org\/10.1016\/j.jsc.2016.07.010","journal-title":"J. Symb. Comput."},{"issue":"1","key":"10_CR11","first-page":"151","volume":"2","author":"JG Darboux","year":"1878","unstructured":"Darboux, J.G.: M\u00e9moire sur les \u00e9quations diff\u00e9rentielles alg\u00e9briques du premier ordre et du premier degr\u00e9. Bull. Sci. Math. 2(1), 151\u2013200 (1878)","journal-title":"Bull. Sci. Math."},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-319-06410-9_14","volume-title":"FM 2014: Formal Methods","author":"W Denman","year":"2014","unstructured":"Denman, W., Mu\u00f1oz, C.: Automated real proving in PVS via MetiTarski. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 194\u2013199. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-06410-9_14"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-66107-0_14","volume-title":"Interactive Theorem Proving","author":"N Fulton","year":"2017","unstructured":"Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: tactical theorem proving for\u00a0hybrid systems. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 207\u2013224. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66107-0_14"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera\u00a0X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"issue":"7","key":"10_CR16","doi-asserted-by":"publisher","first-page":"2003","DOI":"10.1109\/TAC.2017.2763785","volume":"63","author":"T Gan","year":"2018","unstructured":"Gan, T., Chen, M., Li, Y., Xia, B., Zhan, N.: Reachability analysis for solvable dynamical systems. IEEE Trans. Autom. Control 63(7), 2003\u20132018 (2018). \nhttps:\/\/doi.org\/10.1109\/TAC.2017.2763785","journal-title":"IEEE Trans. Autom. Control"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-54862-8_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Ghorbal","year":"2014","unstructured":"Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 279\u2013294. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_19"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.cl.2015.11.003","volume":"47","author":"K Ghorbal","year":"2017","unstructured":"Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput. Lang. Syst. Struct. 47, 19\u201343 (2017). \nhttps:\/\/doi.org\/10.1016\/j.cl.2015.11.003","journal-title":"Comput. Lang. Syst. Struct."},{"key":"10_CR19","doi-asserted-by":"publisher","DOI":"10.1142\/3846","volume-title":"Integrability and Nonintegrability of Dynamical Systems","author":"A Goriely","year":"2001","unstructured":"Goriely, A.: Integrability and Nonintegrability of Dynamical Systems. World Scientific, Hackensack (2001). \nhttps:\/\/doi.org\/10.1142\/3846"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-70545-1_18","volume-title":"Computer Aided Verification","author":"S Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190\u2013203. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-70545-1_18"},{"key":"10_CR21","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. Ph.D. thesis, Universit\u00e9 de Paris, Facult\u00e9 des Sciences (1930)"},{"key":"10_CR22","unstructured":"Immler, F., et al.: ARCH-COMP18 category report: continuous and hybrid systems with nonlinear dynamics. In: Frehse, G., Althoff, M., Bogomolov, S., Johnson, T.T. (eds.) ARCH 2018. EPiC Series in Computing, vol. 54, pp. 53\u201370. EasyChair (2018)"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Arechiga, N.: Simulation-guided Lyapunov analysis for hybrid dynamical systems. In: Fr\u00e4nzle, M., Lygeros, J. (eds.) HSCC 2014, pp. 133\u2013142. ACM (2014). \nhttps:\/\/doi.org\/10.1145\/2562059.2562139","DOI":"10.1145\/2562059.2562139"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Kong, H., Bogomolov, S., Schilling, C., Jiang, Y., Henzinger, T.A.: Safety verification of nonlinear hybrid systems based on invariant clusters. In: Frehse, G., Mitra, S. (eds.) HSCC 2017, pp. 163\u2013172. ACM (2017). \nhttps:\/\/doi.org\/10.1145\/3049797.3049814","DOI":"10.1145\/3049797.3049814"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-39799-8_17","volume-title":"Computer Aided Verification","author":"H Kong","year":"2013","unstructured":"Kong, H., He, F., Song, X., Hung, W.N.N., Gu, M.: Exponential-Condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 242\u2013257. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_17"},{"issue":"3","key":"10_CR26","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231\u2013253 (2001). \nhttps:\/\/doi.org\/10.1006\/jsco.2001.0472","journal-title":"J. Symb. Comput."},{"issue":"1","key":"10_CR27","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10817-017-9424-6","volume":"62","author":"W Li","year":"2019","unstructured":"Li, W., Passmore, G.O., Paulson, L.C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle\/HOL. J. Autom. Reasoning 62(1), 69\u201391 (2019). \nhttps:\/\/doi.org\/10.1007\/s10817-017-9424-6","journal-title":"J. Autom. Reasoning"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17164-2_1","volume-title":"Programming Languages and Systems","author":"J Liu","year":"2010","unstructured":"Liu, J., et al.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1\u201315. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-17164-2_1"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT 2011, pp. 97\u2013106. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/2038642.2038659","DOI":"10.1145\/2038642.2038659"},{"key":"10_CR30","unstructured":"Loeser, T., Iwasaki, Y., Fikes, R.: Safety verification proofs for physical systems. In: Proceedings of the 12th International Workshop on Qualitative Reasoning, pp. 88\u201395 (1998)"},{"issue":"5","key":"10_CR31","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1006\/jsco.1993.1057","volume":"16","author":"Y Man","year":"1993","unstructured":"Man, Y.: Computing closed form solutions of first order ODEs using the Prelle-Singer procedure. J. Symb. Comput. 16(5), 423\u2013443 (1993). \nhttps:\/\/doi.org\/10.1006\/jsco.1993.1057","journal-title":"J. Symb. Comput."},{"key":"10_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4344-1","volume-title":"Algorithmic Algebra","author":"B Mishra","year":"1993","unstructured":"Mishra, B.: Algorithmic Algebra. Springer, Cham (1993). \nhttps:\/\/doi.org\/10.1007\/978-1-4612-4344-1"},{"issue":"1\u20132","key":"10_CR33","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-016-0241-z","volume":"49","author":"S Mitsch","year":"2016","unstructured":"Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1\u20132), 33\u201374 (2016). \nhttps:\/\/doi.org\/10.1007\/s10703-016-0241-z","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"10_CR34","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Platzer, A.: The complete proof theory of hybrid systems. In: LICS 2012, pp. 541\u2013550. IEEE (2012). \nhttps:\/\/doi.org\/10.1109\/LICS.2012.64","DOI":"10.1109\/LICS.2012.64"},{"issue":"1","key":"10_CR36","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/s10703-009-0079-8","volume":"35","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Formal Methods Syst. Des. 35(1), 98\u2013120 (2009). \nhttps:\/\/doi.org\/10.1007\/s10703-009-0079-8","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71070-7_15"},{"key":"10_CR38","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02959-2_35"},{"key":"10_CR39","doi-asserted-by":"publisher","unstructured":"Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: Dawar, A., Gr\u00e4del, E. (eds.) LICS 2018, pp. 819\u2013828. ACM (2018). \nhttps:\/\/doi.org\/10.1145\/3209108.3209147","DOI":"10.1145\/3209108.3209147"},{"key":"10_CR40","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24743-2_32"},{"issue":"1","key":"10_CR41","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1090\/S0002-9947-1983-0704611-X","volume":"279","author":"MJ Prelle","year":"1983","unstructured":"Prelle, M.J., Singer, M.F.: Elementary first integrals of differential equations. Trans. Am. Math. Soc. 279(1), 215\u2013229 (1983)","journal-title":"Trans. Am. Math. Soc."},{"key":"10_CR42","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.tcs.2015.06.018","volume":"594","author":"R Rebiha","year":"2015","unstructured":"Rebiha, R., Moura, A.V., Matringe, N.: Generating invariants for non-linear hybrid systems. Theor. Comput. Sci. 594, 180\u2013200 (2015). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2015.06.018","journal-title":"Theor. Comput. Sci."},{"key":"10_CR43","doi-asserted-by":"crossref","unstructured":"Renegar, J.: Recent progress on the complexity of the decision problem for the reals. In: Goodman, J.E., Pollack, R., Steiger, W. (eds.) Discrete and Computational Geometry: Papers from the DIMACS Special Year, vol. 6, pp. 287\u2013308. DIMACS\/AMS (1990)","DOI":"10.1090\/dimacs\/006\/20"},{"key":"10_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"590","DOI":"10.1007\/978-3-540-31954-2_38","volume-title":"Hybrid Systems: Computation and Control","author":"E Rodr\u00edguez-Carbonell","year":"2005","unstructured":"Rodr\u00edguez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 590\u2013605. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31954-2_38"},{"key":"10_CR45","series-title":"Applied Mathematical Sciences","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9362-7","volume-title":"Stability Theory by Liapunov\u2019s Direct Method","author":"N Rouche","year":"1977","unstructured":"Rouche, N., Habets, P., Laloy, M.: Stability Theory by Liapunov\u2019s Direct Method. Applied Mathematical Sciences. Springer, Heidelberg (1977). \nhttps:\/\/doi.org\/10.1007\/978-1-4684-9362-7"},{"issue":"2","key":"10_CR46","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/s10703-017-0302-y","volume":"53","author":"P Roux","year":"2018","unstructured":"Roux, P., Voronin, Y., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. Formal Methods Syst. Des. 53(2), 286\u2013312 (2018). \nhttps:\/\/doi.org\/10.1007\/s10703-017-0302-y","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR47","first-page":"1","volume":"23","author":"MF Roy","year":"1996","unstructured":"Roy, M.F.: Basic algorithms in real algebraic geometry and their complexity: from Sturm\u2019s theorem to the existential theory of reals. De Gruyter Expositions Math. 23, 1\u201367 (1996)","journal-title":"De Gruyter Expositions Math."},{"key":"10_CR48","doi-asserted-by":"publisher","unstructured":"Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson, K.H., Yi, W. (eds.) HSCC 2010, pp. 221\u2013230. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1755952.1755984","DOI":"10.1145\/1755952.1755984"},{"issue":"1","key":"10_CR49","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods Syst. Des. 32(1), 25\u201355 (2008). \nhttps:\/\/doi.org\/10.1007\/s10703-007-0046-1","journal-title":"Formal Methods Syst. Des."},{"issue":"1\u20132","key":"10_CR50","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0004-3702(96)00050-1","volume":"92","author":"B Shults","year":"1997","unstructured":"Shults, B., Kuipers, B.: Proving properties of continuous systems: qualitative simulation and temporal logic. Artif. Intell. 92(1\u20132), 91\u2013129 (1997). \nhttps:\/\/doi.org\/10.1016\/S0004-3702(96)00050-1","journal-title":"Artif. Intell."},{"key":"10_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-662-49122-5_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Sogokon","year":"2016","unstructured":"Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A method for invariant generation for polynomial continuous systems. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 268\u2013288. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49122-5_13"},{"key":"10_CR52","unstructured":"Sogokon, A., Ghorbal, K., Johnson, T.T.: Non-linear continuous systems for safety verification. In: Frehse, G., Althoff, M. (eds.) ARCH 2016. EPiC Series in Computing, vol. 43, pp. 42\u201351. EasyChair (2016)"},{"key":"10_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-319-95582-7_25","volume-title":"Formal Methods","author":"A Sogokon","year":"2018","unstructured":"Sogokon, A., Ghorbal, K., Tan, Y.K., Platzer, A.: Vector barrier certificates and comparison systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 418\u2013437. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-95582-7_25"},{"key":"10_CR54","volume-title":"Nonlinear Dynamics And Chaos. Studies in Nonlinearity","author":"SH Strogatz","year":"2001","unstructured":"Strogatz, S.H.: Nonlinear Dynamics And Chaos. Studies in Nonlinearity. Westview Press, Boulder (2001)"},{"key":"10_CR55","doi-asserted-by":"publisher","unstructured":"Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: Schost, \u00c9., Emiris, I.Z. (eds.) ISSAC 2011, pp. 329\u2013336. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/1993886.1993935","DOI":"10.1145\/1993886.1993935"},{"key":"10_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/3-540-36580-X_37","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2003","unstructured":"Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514\u2013525. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-36580-X_37"},{"issue":"1","key":"10_CR57","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10703-007-0044-3","volume":"32","author":"A Tiwari","year":"2008","unstructured":"Tiwari, A.: Abstractions for hybrid systems. Formal Methods Syst. Des. 32(1), 57\u201383 (2008). \nhttps:\/\/doi.org\/10.1007\/s10703-007-0044-3","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-540-78929-1_58","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2008","unstructured":"Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 658\u2013661. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78929-1_58"},{"key":"10_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2002","unstructured":"Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465\u2013478. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45873-5_36"},{"key":"10_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-540-24743-2_40","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2004","unstructured":"Tiwari, A., Khanna, G.: Nonlinear systems: approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600\u2013614. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24743-2_40"},{"key":"10_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-25423-4_25"},{"issue":"2","key":"10_CR62","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.entcs.2005.12.007","volume":"144","author":"T Weber","year":"2006","unstructured":"Weber, T.: Integrating a SAT solver with an LCF-style theorem prover. Electron. Notes Theor. Comput. Sci. 144(2), 67\u201378 (2006). \nhttps:\/\/doi.org\/10.1016\/j.entcs.2005.12.007","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"5","key":"10_CR63","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T Weber","year":"2011","unstructured":"Weber, T.: SMT solvers: new oracles for the HOL theorem prover. STTT 13(5), 419\u2013429 (2011). \nhttps:\/\/doi.org\/10.1007\/s10009-011-0188-8","journal-title":"STTT"},{"key":"10_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/978-3-319-48989-6_44","volume-title":"FM 2016: Formal Methods","author":"Z Yang","year":"2016","unstructured":"Yang, Z., Huang, C., Chen, X., Lin, W., Liu, Z.: A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 721\u2013738. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_44"},{"issue":"5","key":"10_CR65","doi-asserted-by":"publisher","first-page":"373","DOI":"10.2514\/1.44289","volume":"6","author":"MH Zaki","year":"2009","unstructured":"Zaki, M.H., Denman, W., Tahar, S., Bois, G.: Integrating abstraction techniques for formal verification of analog designs. J. Aeros. Comp. Inf. Com. 6(5), 373\u2013392 (2009). \nhttps:\/\/doi.org\/10.2514\/1.44289","journal-title":"J. Aeros. Comp. Inf. Com."},{"issue":"1\u20132","key":"10_CR66","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0004-3702(94)90078-7","volume":"69","author":"F Zhao","year":"1994","unstructured":"Zhao, F.: Extracting and representing qualitative behaviors of complex systems in phase space. Artif. Intell. 69(1\u20132), 51\u201392 (1994). \nhttps:\/\/doi.org\/10.1016\/0004-3702(94)90078-7","journal-title":"Artif. Intell."}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T06:07:50Z","timestamp":1588658870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":66,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}