{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:16:24Z","timestamp":1775873784303,"version":"3.50.1"},"reference-count":99,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T00:00:00Z","timestamp":1611100800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T00:00:00Z","timestamp":1611100800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1739629"],"award-info":[{"award-number":["CNS-1739629"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["DGE-1252522"],"award-info":[{"award-number":["DGE-1252522"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-16-1-0288"],"award-info":[{"award-number":["FA9550-16-1-0288"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["DGE1745016"],"award-info":[{"award-number":["DGE1745016"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Continuous invariants<\/jats:italic> are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. <jats:italic>Automatic generation<\/jats:italic> of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop <jats:italic>Pegasus<\/jats:italic>: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera\u00a0X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.\n<\/jats:p>","DOI":"10.1007\/s10703-020-00355-z","type":"journal-article","created":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T12:03:19Z","timestamp":1611144199000},"page":"5-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Pegasus: sound continuous invariant generation"],"prefix":"10.1007","volume":"58","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":[[2021,1,20]]},"reference":[{"key":"355_CR1","doi-asserted-by":"publisher","unstructured":"Almagor S, Kelmendi E, Ouaknine J, Worrell J (2020) Invariants for continuous linear dynamical systems. In: ICALP, LIPIcs, vol 168, pp 107:1\u2013107:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2020.107","DOI":"10.4230\/LIPIcs.ICALP.2020.107"},{"issue":"7","key":"355_CR2","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur R, Henzinger TA, Lafferriere G, Pappas GJ (2000) Discrete abstractions of hybrid systems. Proc IEEE 88(7):971\u2013984. https:\/\/doi.org\/10.1109\/5.871304","journal-title":"Proc IEEE"},{"key":"355_CR3","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 CM (1992) Dynamical systems: differential equations, maps, and chaotic behaviour, vol 5. CRC Press, Boca Raton"},{"key":"355_CR4","doi-asserted-by":"publisher","unstructured":"Beckert B, Giese M, H\u00e4hnle R, Klebanov V, R\u00fcmmer P, Schlager S, Schmitt PH (2007) The KeY system 1.0 (deduction component). In: Pfenning F (ed) CADE, LNCS, vol 4603, pp 379\u2013384. Springer. https:\/\/doi.org\/10.1007\/978-3-540-73595-3_26","DOI":"10.1007\/978-3-540-73595-3_26"},{"issue":"1","key":"355_CR5","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1137\/0301003","volume":"1","author":"R Bellman","year":"1962","unstructured":"Bellman R (1962) Vector Lyapunov functions. SIAM J Control Optim 1(1):32\u201334. https:\/\/doi.org\/10.1137\/0301003","journal-title":"SIAM J Control Optim"},{"key":"355_CR6","doi-asserted-by":"publisher","unstructured":"Ben\u00a0Sassi MA, Girard A, Sankaranarayanan S (2014) Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: CDC, pp 6348\u20136353. IEEE. https:\/\/doi.org\/10.1109\/CDC.2014.7040384","DOI":"10.1109\/CDC.2014.7040384"},{"key":"355_CR7","doi-asserted-by":"publisher","unstructured":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H (2017) Conic abstractions for hybrid systems. In: Abate A, Geeraerts G (eds) FORMATS, LNCS, vol 10419, pp 116\u2013132. Springer. https:\/\/doi.org\/10.1007\/978-3-319-65765-3_7","DOI":"10.1007\/978-3-319-65765-3_7"},{"key":"355_CR8","doi-asserted-by":"publisher","unstructured":"B\u00f6hme S, Weber T (2010) Fast LCF-style proof reconstruction for Z3. In: Kaufmann M, Paulson LC (eds) ITP, LNCS, vol 6172, pp 179\u2013194. Springer. https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"355_CR9","doi-asserted-by":"publisher","unstructured":"Bohrer B, Fern\u00e1ndez M, Platzer A (2019) dL$$_\\iota $$: Definite descriptions in differential dynamic logic. In: Fontaine P (ed) CADE, LNCS, vol 11716, pp 94\u2013110. Springer. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_6","DOI":"10.1007\/978-3-030-29436-6_6"},{"key":"355_CR10","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1145\/3192366.3192406","volume-title":"PLDI","author":"B Bohrer","year":"2018","unstructured":"Bohrer B, Tan YK, Mitsch S, Myreen MO, Platzer A (2018) VeriPhy: verified controller executables from verified cyber-physical system models. In: Foster JS, Grossman D (eds) PLDI. ACM, New York, pp 617\u2013630. https:\/\/doi.org\/10.1145\/3192366.3192406"},{"key":"355_CR11","doi-asserted-by":"publisher","unstructured":"Boreale M (2020) Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODEs. Science of Computer Programming 193. https:\/\/doi.org\/10.1016\/j.scico.2020.102441","DOI":"10.1016\/j.scico.2020.102441"},{"key":"355_CR12","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-319-48628-4_3","volume-title":"Provably correct systems, NASA monographs in systems and software engineering","author":"M Chen","year":"2017","unstructured":"Chen M, Han X, Tang T, Wang S, Yang M, Zhan N, Zhao H, Zou L (2017) MARS: a toolchain for modelling, analysis and verification of hybrid systems. In: Hinchey MG, Bowen JP, Olderog E (eds) Provably correct systems, NASA monographs in systems and software engineering. Springer, Berlin, pp 39\u201358. https:\/\/doi.org\/10.1007\/978-3-319-48628-4_3"},{"key":"355_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-35794-7","volume-title":"Ordinary differential equations with applications","author":"C Chicone","year":"2006","unstructured":"Chicone C (2006) Ordinary differential equations with applications, 2nd edn. Springer, New York. https:\/\/doi.org\/10.1007\/0-387-35794-7","edition":"2"},{"key":"355_CR14","doi-asserted-by":"publisher","unstructured":"Collins GE (1975) Quantifier elimination for real closed fields by cylindrical algebraic decompostion, LNCS, vol 33, pp 134\u2013183. Springer. https:\/\/doi.org\/10.1007\/3-540-07407-4_17","DOI":"10.1007\/3-540-07407-4_17"},{"key":"355_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16721-3","volume-title":"Ideals, varieties, and algorithms","author":"DA Cox","year":"2015","unstructured":"Cox DA, Little J, O\u2019Shea D (2015) Ideals, varieties, and algorithms, 4th edn. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-319-16721-3","edition":"4"},{"key":"355_CR16","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 (2017) Barrier certificates revisited. J Symb Comput 80:62\u201386. https:\/\/doi.org\/10.1016\/j.jsc.2016.07.010","journal-title":"J Symb Comput"},{"issue":"1","key":"355_CR17","first-page":"151","volume":"2","author":"JG Darboux","year":"1878","unstructured":"Darboux JG (1878) M\u00e9moire sur les \u00e9quations diff\u00e9rentielles alg\u00e9briques du premier ordre et du premier degr\u00e9. Bull Sci Math 2(1):151\u2013200","journal-title":"Bull Sci Math"},{"key":"355_CR18","doi-asserted-by":"publisher","unstructured":"Denman W, Mu\u00f1oz CA (2014) Automated real proving in PVS via MetiTarski. In: Jones CB, Pihlajasaari P, Sun J (eds) FM, LNCS, vol 8442, pp 194\u2013199. Springer. https:\/\/doi.org\/10.1007\/978-3-319-06410-9_14","DOI":"10.1007\/978-3-319-06410-9_14"},{"key":"355_CR19","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.automatica.2016.12.013","volume":"78","author":"A Djaballah","year":"2017","unstructured":"Djaballah A, Chapoutot A, Kieffer M, Bouissou O (2017) Construction of parametric barrier functions for dynamical systems using interval analysis. Automatica 78:287\u2013296. https:\/\/doi.org\/10.1016\/j.automatica.2016.12.013","journal-title":"Automatica"},{"key":"355_CR20","doi-asserted-by":"publisher","unstructured":"Dutertre B, de\u00a0Moura LM (2006) A fast linear-arithmetic solver for DPLL(T). In: Ball T, Jones RB (eds) CAV, LNCS, vol 4144, pp 81\u201394. Springer. https:\/\/doi.org\/10.1007\/11817963_11","DOI":"10.1007\/11817963_11"},{"issue":"2","key":"355_CR21","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF02970860","volume":"4","author":"M Falconi","year":"2004","unstructured":"Falconi M, Llibre J (2004) $$n-1$$ independent first integrals for linear differential systems in $${\\mathbb{R}}^n$$ and $${\\mathbb{C}}^n$$. Qual Theory Dyn Syst 4(2):233\u2013254. https:\/\/doi.org\/10.1007\/BF02970860","journal-title":"Qual Theory Dyn Syst"},{"issue":"1\u20132","key":"355_CR22","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s12346-010-0021-x","volume":"9","author":"A Ferragut","year":"2010","unstructured":"Ferragut A, Giacomini H (2010) A new algorithm for finding rational first integrals of polynomial vector fields. Qual Theory Dyn Syst 9(1\u20132):89\u201399. https:\/\/doi.org\/10.1007\/s12346-010-0021-x","journal-title":"Qual Theory Dyn Syst"},{"key":"355_CR23","doi-asserted-by":"publisher","unstructured":"Frehse G, Le\u00a0Guernic C, Donz\u00e9 A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan G, Qadeer S (eds) CAV, LNCS, vol 6806, pp 379\u2013395. Springer. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"355_CR24","doi-asserted-by":"publisher","unstructured":"Fulton N, Mitsch S, Bohrer B, Platzer A (2017) Bellerophon: tactical theorem proving for hybrid systems. In: Ayala-Rinc\u00f3n M, Mu\u00f1oz CA (eds) ITP, LNCS, vol 10499, pp 207\u2013224. Springer. https:\/\/doi.org\/10.1007\/978-3-319-66107-0_14","DOI":"10.1007\/978-3-319-66107-0_14"},{"key":"355_CR25","doi-asserted-by":"publisher","unstructured":"Fulton N, Mitsch S, Quesel J, V\u00f6lp M, Platzer A (2015) KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty AP, Middeldorp A (eds) CADE, LNCS, vol 9195, pp 527\u2013538. Springer. https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36","DOI":"10.1007\/978-3-319-21401-6_36"},{"issue":"7","key":"355_CR26","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 (2018) Reachability analysis for solvable dynamical systems. IEEE Trans Autom Control 63(7):2003\u20132018. https:\/\/doi.org\/10.1109\/TAC.2017.2763785","journal-title":"IEEE Trans Autom Control"},{"key":"355_CR27","doi-asserted-by":"publisher","unstructured":"Ghorbal K, Platzer A (2014) Characterizing algebraic invariants by differential radical invariants. In: \u00c1brah\u00e1m E, Havelund K (eds) TACAS, LNCS, vol 8413, pp 279\u2013294. Springer. https:\/\/doi.org\/10.1007\/978-3-642-54862-8_19","DOI":"10.1007\/978-3-642-54862-8_19"},{"issue":"1","key":"355_CR28","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 (2017) A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput Lang Syst Struct 47(1):19\u201343. https:\/\/doi.org\/10.1016\/j.cl.2015.11.003","journal-title":"Comput Lang Syst Struct"},{"key":"355_CR29","doi-asserted-by":"publisher","unstructured":"Goebel R, Hespanha J, Teel AR, Cai C, Sanfelice R (2004) Hybrid systems: generalized solutions and robust stability. In: NOLCOS, vol\u00a037, pp 1\u201312. Stuttgart, Germany. https:\/\/doi.org\/10.1016\/S1474-6670(17)31194-1","DOI":"10.1016\/S1474-6670(17)31194-1"},{"key":"355_CR30","unstructured":"Gorbuzov VN, Pranevich AF (2012) First integrals of ordinary linear differential systems. CoRR arXiv:1201.4141"},{"key":"355_CR31","doi-asserted-by":"publisher","unstructured":"Goriely A (2001) Integrability and nonintegrability of dynamical systems. World Scientific. https:\/\/doi.org\/10.1142\/3846","DOI":"10.1142\/3846"},{"key":"355_CR32","doi-asserted-by":"publisher","unstructured":"Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Gupta A, Malik S (eds) CAV, LNCS, vol 5123, pp 190\u2013203. Springer. https:\/\/doi.org\/10.1007\/978-3-540-70545-1_18","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"355_CR33","doi-asserted-by":"publisher","DOI":"10.1515\/9781400841042","volume-title":"Nonlinear dynamical systems and control: a Lyapunov-based approach","author":"WM Haddad","year":"2008","unstructured":"Haddad WM, Chellaboina V (2008) Nonlinear dynamical systems and control: a Lyapunov-based approach. Princeton University Press, Princeton"},{"key":"355_CR34","volume-title":"Recherches sur la th\u00e9orie de la d\u00e9monstration","author":"J Herbrand","year":"1930","unstructured":"Herbrand J (1930) Recherches sur la th\u00e9orie de la d\u00e9monstration. Universit\u00e9 de Paris, Facult\u00e9 des Sciences, Doctorat d\u2019\u00e9tat"},{"key":"355_CR35","unstructured":"Immler F, Althoff M, Chen X, Fan C, Frehse G, Kochdumper N, Li Y, Mitra S, Tomar MS, Zamani M (2018) ARCH-COMP18 category report: continuous and hybrid systems with nonlinear dynamics. In: Frehse G, Althoff M, Bogomolov S, Johnson TT (eds) ARCH, EPiC series in computing, vol 54. EasyChair, pp 53\u201370"},{"key":"355_CR36","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/2562059.2562139","volume-title":"HSCC","author":"J Kapinski","year":"2014","unstructured":"Kapinski J, Deshmukh JV, Sankaranarayanan S, Arechiga N (2014) Simulation-guided Lyapunov analysis for hybrid dynamical systems. In: Fr\u00e4nzle M, Lygeros J (eds) HSCC. ACM, New York, pp 133\u2013142. https:\/\/doi.org\/10.1145\/2562059.2562139"},{"issue":"2","key":"355_CR37","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1090\/S0002-9947-1925-1501305-1","volume":"27","author":"E Kasner","year":"1925","unstructured":"Kasner E (1925) Solutions of the Einstein equations involving functions of only one variable. Trans Am Math Soc 27(2):155\u2013162. https:\/\/doi.org\/10.1090\/S0002-9947-1925-1501305-1","journal-title":"Trans Am Math Soc"},{"key":"355_CR38","volume-title":"Nonlinear systems","author":"HK Khalil","year":"1992","unstructured":"Khalil HK (1992) Nonlinear systems. Macmillan Publishing Company, New York"},{"key":"355_CR39","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/3049797.3049814","volume-title":"HSCC","author":"H Kong","year":"2017","unstructured":"Kong H, Bogomolov S, Schilling C, Jiang Y, Henzinger TA (2017) Safety verification of nonlinear hybrid systems based on invariant clusters. In: Frehse G, Mitra S (eds) HSCC. ACM, New York, pp 163\u2013172. https:\/\/doi.org\/10.1145\/3049797.3049814"},{"key":"355_CR40","doi-asserted-by":"publisher","unstructured":"Kong H, He F, Song X, Hung WNN, Gu M (2013) Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina N, Veith H (eds) CAV, LNCS, vol 8044, pp 242\u2013257. Springer. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_17","DOI":"10.1007\/978-3-642-39799-8_17"},{"key":"355_CR41","doi-asserted-by":"publisher","unstructured":"Kong S, Gao S, Chen W, Clarke EM (2015) dReach: $$\\delta $$-reachability analysis for hybrid systems. In: Baier C, Tinelli C (eds) TACAS, LNCS, vol 9035, pp 200\u2013205. Springer. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_15","DOI":"10.1007\/978-3-662-46681-0_15"},{"issue":"3","key":"355_CR42","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere G, Pappas GJ, Yovine S (2001) Symbolic reachability computation for families of linear vector fields. J Symb Comput 32(3):231\u2013253. https:\/\/doi.org\/10.1006\/jsco.2001.0472","journal-title":"J Symb Comput"},{"key":"355_CR43","doi-asserted-by":"publisher","unstructured":"Liu J, Lv J, Quan Z, Zhan N, Zhao H, Zhou C, Zou L (2010) A calculus for hybrid CSP. In: Ueda K (ed) APLAS, LNCS, vol 6461, pp 1\u201315. Springer. https:\/\/doi.org\/10.1007\/978-3-642-17164-2_1","DOI":"10.1007\/978-3-642-17164-2_1"},{"key":"355_CR44","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/2038642.2038659","volume-title":"EMSOFT","author":"J Liu","year":"2011","unstructured":"Liu J, Zhan N, Zhao H (2011) Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty S, Jerraya A, Baruah SK, Fischmeister S (eds) EMSOFT. ACM, New York, pp 97\u2013106. https:\/\/doi.org\/10.1145\/2038642.2038659"},{"issue":"3","key":"355_CR45","doi-asserted-by":"publisher","first-page":"1622","DOI":"10.1063\/1.1435078","volume":"43","author":"J Llibre","year":"2002","unstructured":"Llibre J, Zhang X (2002) Invariant algebraic surfaces of the Lorenz system. J Math Phys 43(3):1622\u20131645. https:\/\/doi.org\/10.1063\/1.1435078","journal-title":"J Math Phys"},{"key":"355_CR46","unstructured":"Loeser T, Iwasaki Y, Fikes R (1998) Safety verification proofs for physical systems. In: Proc. of the 12th intl. workshop on qualitative reasoning, pp 88\u201395"},{"issue":"5","key":"355_CR47","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1006\/jsco.1993.1057","volume":"16","author":"Y Man","year":"1993","unstructured":"Man Y (1993) Computing closed form solutions of first order ODEs using the Prelle\u2013Singer procedure. J Symb Comput 16(5):423\u2013443. https:\/\/doi.org\/10.1006\/jsco.1993.1057","journal-title":"J Symb Comput"},{"issue":"10","key":"355_CR48","doi-asserted-by":"publisher","first-page":"L329","DOI":"10.1088\/0305-4470\/27\/10\/005","volume":"27","author":"Y Man","year":"1994","unstructured":"Man Y (1994) First integrals of autonomous systems of differential equations and the Prelle\u2013Singer procedure. J Phys A Math Gen 27(10):L329\u2013L332. https:\/\/doi.org\/10.1088\/0305-4470\/27\/10\/005","journal-title":"J Phys A Math Gen"},{"key":"355_CR49","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4344-1","volume-title":"Algorithmic algebra","author":"B Mishra","year":"1993","unstructured":"Mishra B (1993) Algorithmic algebra. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-1-4612-4344-1"},{"issue":"1\u20132","key":"355_CR50","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 (2016) ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst Des 49(1\u20132):33\u201374. https:\/\/doi.org\/10.1007\/s10703-016-0241-z","journal-title":"Formal Methods Syst Des"},{"key":"355_CR51","volume-title":"Deductive verification: the state of the future, LNCS","author":"S Mitsch","year":"2020","unstructured":"Mitsch S, Platzer A (2020) A retrospective on developing hybrid systems provers in the KeYmaera family: a tale of three provers. In: Ahrendt W, Bubel R, Beckert B, H\u00e4hnle R, Ulbrich M (eds) Deductive verification: the state of the future, LNCS. Springer, Berlin"},{"key":"355_CR52","doi-asserted-by":"publisher","unstructured":"Olver PJ (2000) Applications of Lie groups to differential equations, graduate texts in mathematics, vol 107, 2nd edn. Springer. https:\/\/doi.org\/10.1007\/978-1-4684-0274-2","DOI":"10.1007\/978-1-4684-0274-2"},{"key":"355_CR53","unstructured":"Papachristodoulou A, Anderson J, Valmorbida G, Prajna S, Seiler P, Parrilo PA (2013) SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB. CoRR arXiv:1310.4716"},{"key":"355_CR54","doi-asserted-by":"publisher","unstructured":"Papachristodoulou A, Prajna S (2002) On the construction of Lyapunov functions using the sum of squares decomposition. In: CDC, vol\u00a03, pp 3482\u20133487. https:\/\/doi.org\/10.1109\/CDC.2002.1184414","DOI":"10.1109\/CDC.2002.1184414"},{"key":"355_CR55","doi-asserted-by":"publisher","unstructured":"Parrilo PA (2000) Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. Ph.D. thesis, California Institute of Technology. https:\/\/doi.org\/10.7907\/2K6Y-CH43","DOI":"10.7907\/2K6Y-CH43"},{"issue":"2","key":"355_CR56","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reason 41(2):143\u2013189. https:\/\/doi.org\/10.1007\/s10817-008-9103-8","journal-title":"J Autom Reason"},{"key":"355_CR57","doi-asserted-by":"publisher","unstructured":"Platzer A (2012) The complete proof theory of hybrid systems. In: LICS, pp 541\u2013550. IEEE Computer Society. https:\/\/doi.org\/10.1109\/LICS.2012.64","DOI":"10.1109\/LICS.2012.64"},{"key":"355_CR58","doi-asserted-by":"publisher","unstructured":"Platzer A (2012) A differential operator approach to equational differential invariants\u2014(invited paper). In: Beringer L, Felty AP (eds) ITP, LNCS, vol 7406, pp 28\u201348. Springer. https:\/\/doi.org\/10.1007\/978-3-642-32347-8_3","DOI":"10.1007\/978-3-642-32347-8_3"},{"key":"355_CR59","doi-asserted-by":"publisher","unstructured":"Platzer A (2012) Logics of dynamical systems. In: LICS, pp 13\u201324. IEEE Computer Society. https:\/\/doi.org\/10.1109\/LICS.2012.13","DOI":"10.1109\/LICS.2012.13"},{"issue":"2","key":"355_CR60","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2017","unstructured":"Platzer A (2017) A complete uniform substitution calculus for differential dynamic logic. J Autom Reason 59(2):219\u2013265. https:\/\/doi.org\/10.1007\/s10817-016-9385-1","journal-title":"J Autom Reason"},{"issue":"1","key":"355_CR61","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 EM (2009) Computing differential invariants of hybrid systems as fixedpoints. Formal Methods Syst Des 35(1):98\u2013120. https:\/\/doi.org\/10.1007\/s10703-009-0079-8","journal-title":"Formal Methods Syst Des"},{"key":"355_CR62","doi-asserted-by":"publisher","unstructured":"Platzer A, Quesel J (2008) KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando A, Baumgartner P, Dowek G (eds) IJCAR, LNCS, vol 5195, pp 171\u2013178. Springer. https:\/\/doi.org\/10.1007\/978-3-540-71070-7_15","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"355_CR63","doi-asserted-by":"publisher","unstructured":"Platzer A, Quesel J, R\u00fcmmer P (2009) Real world verification. In: Schmidt RA (ed) CADE, LNCS, vol 5663, pp 485\u2013501. Springer. https:\/\/doi.org\/10.1007\/978-3-642-02959-2_35","DOI":"10.1007\/978-3-642-02959-2_35"},{"key":"355_CR64","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3380825","volume":"67","author":"A Platzer","year":"2020","unstructured":"Platzer A, Tan YK (2020) Differential equation invariance axiomatization. J ACM 67:1. https:\/\/doi.org\/10.1145\/3380825","journal-title":"J ACM"},{"key":"355_CR65","doi-asserted-by":"publisher","DOI":"10.1016\/C2013-0-01692-1","volume-title":"Ordinary differential equations","author":"LS Pontryagin","year":"1962","unstructured":"Pontryagin LS (1962) Ordinary differential equations. Pergamon Press, Oxford. https:\/\/doi.org\/10.1016\/C2013-0-01692-1"},{"key":"355_CR66","doi-asserted-by":"publisher","unstructured":"Prajna S, Jadbabaie A (2004) Safety verification of hybrid systems using barrier certificates. In: Alur R, Pappas GJ (eds) HSCC, LNCS, vol 2993, pp 477\u2013492. Springer. https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32","DOI":"10.1007\/978-3-540-24743-2_32"},{"issue":"1","key":"355_CR67","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1090\/S0002-9947-1983-0704611-X","volume":"279","author":"MJ Prelle","year":"1983","unstructured":"Prelle MJ, Singer MF (1983) Elementary first integrals of differential equations. Trans Am Math Soc 279(1):215\u2013229. https:\/\/doi.org\/10.1090\/S0002-9947-1983-0704611-X","journal-title":"Trans Am Math Soc"},{"key":"355_CR68","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 AV, Matringe N (2015) Generating invariants for non-linear hybrid systems. Theor Comput Sci 594:180\u2013200. https:\/\/doi.org\/10.1016\/j.tcs.2015.06.018","journal-title":"Theor Comput Sci"},{"key":"355_CR69","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-7091-9459-1_11","volume-title":"Discrete and computational geometry: papers from the DIMACS special year","author":"J Renegar","year":"1990","unstructured":"Renegar J (1990) Recent progress on the complexity of the decision problem for the reals. In: Goodman JE, Pollack R, Steiger W (eds) Discrete and computational geometry: papers from the DIMACS special year, vol 6. DIMACS\/AMS, New York, pp 287\u2013308. https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_11"},{"key":"355_CR70","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez-Carbonell E, Tiwari A (2005) Generating polynomial invariants for hybrid systems. In: Morari M, Thiele L (eds) HSCC, LNCS, vol 3414, pp 590\u2013605. Springer. https:\/\/doi.org\/10.1007\/978-3-540-31954-2_38","DOI":"10.1007\/978-3-540-31954-2_38"},{"key":"355_CR71","doi-asserted-by":"publisher","unstructured":"Rouche N, Habets P, Laloy M (1977) Stability theory by Liapunov\u2019s direct method, Appl. Math. Sci., vol\u00a022. Springer. https:\/\/doi.org\/10.1007\/978-1-4684-9362-7","DOI":"10.1007\/978-1-4684-9362-7"},{"issue":"2","key":"355_CR72","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 (2018) Validating numerical semidefinite programming solvers for polynomial invariants. Form Methods Syst Des 53(2):286\u2013312. https:\/\/doi.org\/10.1007\/s10703-017-0302-y","journal-title":"Form Methods Syst Des"},{"key":"355_CR73","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1515\/9783110811117","volume":"23","author":"MF Roy","year":"1996","unstructured":"Roy MF (1996) Basic algorithms in real algebraic geometry and their complexity: from Sturm\u2019s theorem to the existential theory of reals. De Gruyter Expos Math 23:1\u201367. https:\/\/doi.org\/10.1515\/9783110811117","journal-title":"De Gruyter Expos Math"},{"key":"355_CR74","first-page":"221","volume-title":"HSCC","author":"S Sankaranarayanan","year":"2010","unstructured":"Sankaranarayanan S (2010) Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson KH, Yi W (eds) HSCC. ACM, New York, pp 221\u2013230"},{"key":"355_CR75","doi-asserted-by":"publisher","unstructured":"Sankaranarayanan S, Chen X, \u00c1brah\u00e1m E (2013) Lyapunov function synthesis using Handelman representations. In: NOLCOS, pp 576\u2013581. https:\/\/doi.org\/10.3182\/20130904-3-FR-2041.00198","DOI":"10.3182\/20130904-3-FR-2041.00198"},{"issue":"1","key":"355_CR76","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 HB, Manna Z (2008) Constructing invariants for hybrid systems. Form Methods Syst Des 32(1):25\u201355. https:\/\/doi.org\/10.1007\/s10703-007-0046-1","journal-title":"Form Methods Syst Des"},{"key":"355_CR77","doi-asserted-by":"publisher","unstructured":"Schlomiuk D (1993) Algebraic and geometric aspects of the theory of polynomial vector fields. In: NATO ASI series, vol 408, pp 429\u2013467. Springer, Netherlands. https:\/\/doi.org\/10.1007\/978-94-015-8238-4_10","DOI":"10.1007\/978-94-015-8238-4_10"},{"issue":"1","key":"355_CR78","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.jmaa.2007.01.060","volume":"335","author":"S Shi","year":"2007","unstructured":"Shi S (2007) On the nonexistence of rational first integrals for nonlinear systems and semiquasihomogeneous systems. J Math Anal Appl 335(1):125\u2013134. https:\/\/doi.org\/10.1016\/j.jmaa.2007.01.060","journal-title":"J Math Anal Appl"},{"issue":"1\u20132","key":"355_CR79","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 (1997) Proving properties of continuous systems: qualitative simulation and temporal logic. Artif Intell 92(1\u20132):91\u2013129. https:\/\/doi.org\/10.1016\/S0004-3702(96)00050-1","journal-title":"Artif Intell"},{"key":"355_CR80","volume-title":"Applied nonlinear control","author":"JJE Slotine","year":"1991","unstructured":"Slotine JJE, Li W (1991) Applied nonlinear control. Prentice-Hall Inc., Upper Saddle River"},{"key":"355_CR81","doi-asserted-by":"publisher","unstructured":"Sogokon A, Ghorbal K, Jackson PB, Platzer A (2016) A method for invariant generation for polynomial continuous systems. In: Jobstmann B, Leino KRM (eds) VMCAI, LNCS, vol 9583, pp 268\u2013288. Springer. https:\/\/doi.org\/10.1007\/978-3-662-49122-5_13","DOI":"10.1007\/978-3-662-49122-5_13"},{"key":"355_CR82","unstructured":"Sogokon A, Ghorbal K, Johnson TT (2016) Non-linear continuous systems for safety verification. In: Frehse G, Althoff M (eds) ARCH, EPiC series in computing, vol 43. EasyChair, pp 42\u201351"},{"key":"355_CR83","doi-asserted-by":"publisher","unstructured":"Sogokon A, Ghorbal K, Tan YK, Platzer A (2018) Vector barrier certificates and comparison systems. In: Havelund K, Peleska J, Roscoe B, de\u00a0Vink EP (eds) FM, LNCS, vol 10951, pp 418\u2013437. Springer. https:\/\/doi.org\/10.1007\/978-3-319-95582-7_25","DOI":"10.1007\/978-3-319-95582-7_25"},{"key":"355_CR84","doi-asserted-by":"publisher","unstructured":"Sogokon A, Mitsch S, Tan YK, Cordwell K, Platzer A (2019) Pegasus: a framework for sound continuous invariant generation. In: ter Beek MH, McIver A, Oliveira JN (eds) FM, LNCS, vol 11800, pp 138\u2013157. Springer. https:\/\/doi.org\/10.1007\/978-3-030-30942-8_10","DOI":"10.1007\/978-3-030-30942-8_10"},{"key":"355_CR85","volume-title":"Nonlinear dynamics and chaos. Studies in nonlinearity","author":"SH Strogatz","year":"2001","unstructured":"Strogatz SH (2001) Nonlinear dynamics and chaos. Studies in nonlinearity. Westview Press, Boulder"},{"key":"355_CR86","doi-asserted-by":"publisher","unstructured":"Sturm T, Tiwari A (2011) Verification and synthesis using real quantifier elimination. In: Schost \u00c9, Emiris IZ (eds) ISSAC, pp 329\u2013336. ACM. https:\/\/doi.org\/10.1145\/1993886.1993935","DOI":"10.1145\/1993886.1993935"},{"key":"355_CR87","doi-asserted-by":"publisher","unstructured":"Tiwari A (2003) Approximate reachability for linear systems. In: Maler O, Pnueli A (eds) HSCC, LNCS, vol 2623, pp 514\u2013525. Springer. https:\/\/doi.org\/10.1007\/3-540-36580-X_37","DOI":"10.1007\/3-540-36580-X_37"},{"issue":"1","key":"355_CR88","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10703-007-0044-3","volume":"32","author":"A Tiwari","year":"2008","unstructured":"Tiwari A (2008) Abstractions for hybrid systems. Form Methods Syst Des 32(1):57\u201383. https:\/\/doi.org\/10.1007\/s10703-007-0044-3","journal-title":"Form Methods Syst Des"},{"key":"355_CR89","doi-asserted-by":"publisher","unstructured":"Tiwari A (2008) Generating box invariants. In: Egerstedt M, Mishra B (eds) HSCC, LNCS, vol 4981, pp 658\u2013661. Springer. https:\/\/doi.org\/10.1007\/978-3-540-78929-1_58","DOI":"10.1007\/978-3-540-78929-1_58"},{"key":"355_CR90","doi-asserted-by":"publisher","unstructured":"Tiwari A, Khanna G (2002) Series of abstractions for hybrid automata. In: Tomlin C, Greenstreet MR (eds) HSCC, LNCS, vol 2289, pp 465\u2013478. Springer. https:\/\/doi.org\/10.1007\/3-540-45873-5_36","DOI":"10.1007\/3-540-45873-5_36"},{"key":"355_CR91","doi-asserted-by":"publisher","unstructured":"Tiwari A, Khanna G (2004) Nonlinear systems: approximating reach sets. In: Alur R, Pappas GJ (eds) HSCC, LNCS, vol 2993, pp 600\u2013614. Springer. https:\/\/doi.org\/10.1007\/978-3-540-24743-2_40","DOI":"10.1007\/978-3-540-24743-2_40"},{"key":"355_CR92","doi-asserted-by":"publisher","unstructured":"Wang S, Zhan N, Zou L (2015) An improved HHL prover: an interactive theorem prover for hybrid systems. In Butler MJ, Conchon S, Za\u00efdi F (eds) ICFEM, LNCS, vol 9407, pp 382\u2013399. Springer. https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25","DOI":"10.1007\/978-3-319-25423-4_25"},{"issue":"2","key":"355_CR93","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 (2006) Integrating a SAT solver with an LCF-style theorem prover. Electr Notes Theor Comput Sci 144(2):67\u201378. https:\/\/doi.org\/10.1016\/j.entcs.2005.12.007","journal-title":"Electr Notes Theor Comput Sci"},{"issue":"5","key":"355_CR94","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T Weber","year":"2011","unstructured":"Weber T (2011) SMT solvers: new oracles for the HOL theorem prover. STTT 13(5):419\u2013429. https:\/\/doi.org\/10.1007\/s10009-011-0188-8","journal-title":"STTT"},{"key":"355_CR95","doi-asserted-by":"publisher","unstructured":"Yang Z, Huang C, Chen X, Lin W, Liu Z (2016) A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM, LNCS, vol 9995, pp 721\u2013738. https:\/\/doi.org\/10.1007\/978-3-319-48989-6_44","DOI":"10.1007\/978-3-319-48989-6_44"},{"key":"355_CR96","doi-asserted-by":"publisher","first-page":"100837","DOI":"10.1016\/j.nahs.2019.100837","volume":"36","author":"Z Yang","year":"2020","unstructured":"Yang Z, Wu M, Lin W (2020) An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems. Nonlinear Anal Hybrid Syst 36:100837. https:\/\/doi.org\/10.1016\/j.nahs.2019.100837","journal-title":"Nonlinear Anal Hybrid Syst"},{"issue":"5","key":"355_CR97","doi-asserted-by":"publisher","first-page":"373","DOI":"10.2514\/1.44289","volume":"6","author":"MH Zaki","year":"2009","unstructured":"Zaki MH, Denman W, Tahar S, Bois G (2009) Integrating abstraction techniques for formal verification of analog designs. J Aerosp Comput Inf Commun 6(5):373\u2013392. https:\/\/doi.org\/10.2514\/1.44289","journal-title":"J Aerosp Comput Inf Commun"},{"key":"355_CR98","doi-asserted-by":"publisher","unstructured":"Zhang X (2017) Integrability of dynamical systems: algebra and analysis. Developments in Mathematics, vol\u00a047. Springer. https:\/\/doi.org\/10.1007\/978-981-10-4226-3","DOI":"10.1007\/978-981-10-4226-3"},{"issue":"1\u20132","key":"355_CR99","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 (1994) Extracting and representing qualitative behaviors of complex systems in phase space. Artif Intell 69(1\u20132):51\u201392. https:\/\/doi.org\/10.1016\/0004-3702(94)90078-7","journal-title":"Artif Intell"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00355-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00355-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00355-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T15:50:29Z","timestamp":1661529029000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00355-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,20]]},"references-count":99,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["355"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00355-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,20]]},"assertion":[{"value":"18 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 November 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 January 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}