{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:25:27Z","timestamp":1750843527569,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_14","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"207-224","source":"Crossref","is-referenced-by-count":19,"title":["Bellerophon: Tactical Theorem Proving for\u00a0Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Nathan","family":"Fulton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rose","family":"Bohrer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"LM de Moura","year":"2015","unstructured":"de Moura, L.M., Kong, S., Avigad, J., Doorn, F., Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 378\u2013388. Springer, Cham (2015). doi:10.1007\/978-3-319-21401-6_26"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., et al. (eds.) [13], pp. 209\u2013229","DOI":"10.1007\/3-540-57318-6_30"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-39320-4_29","volume-title":"Intelligent Computer Mathematics","author":"B Barras","year":"2013","unstructured":"Barras, B., Carmen Gonz\u00e1lez Huesca, L., Herbelin, H., R\u00e9gis-Gianas, Y., Tassi, E., Wenzel, M., Wolff, B.: Pervasive parallelism in highly-trustable interactive theorem proving systems. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 359\u2013363. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39320-4_29"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bohrer, R., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Certified Programs and Proofs - 6th ACM SIGPLAN Conference, CPP 2017, pp. 208\u2013221. ACM (2017)","DOI":"10.1145\/3018610.3018616"},{"issue":"1","key":"14_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015)","journal-title":"Math. Comput. Sci."},{"key":"14_CR6","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"issue":"3","key":"14_CR7","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"GE Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"key":"14_CR8","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"RL Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, M., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Upper Saddle River (1986)"},{"issue":"1\/2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1\/2), 29\u201335 (1988)","journal-title":"J. Symb. Comput."},{"issue":"3","key":"14_CR10","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3), 263\u2013279 (2008)","journal-title":"STTT"},{"key":"14_CR11","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). doi:10.1007\/978-3-642-22110-1_30"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","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 X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 527\u2013538. Springer, Cham (2015). doi:10.1007\/978-3-319-21401-6_36"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57318-6","volume-title":"Hybrid Systems","year":"1993","unstructured":"Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.): Hybrid Systems. LNCS, vol. 736. Springer, Heidelberg (1993). doi:10.1007\/3-540-57318-6"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114\u2013129. Springer, Heidelberg (2005). doi:10.1007\/11541868_8"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/10930755_19","volume-title":"Theorem Proving in Higher Order Logics","author":"J Hickey","year":"2003","unstructured":"Hickey, J., et al.: MetaPRL \u2013 a modular logical environment. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 287\u2013303. Springer, Heidelberg (2003). doi:10.1007\/10930755_19"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-39634-2_21","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2013","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279\u2013294. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39634-2_21"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-43144-4_12","volume-title":"Interactive Theorem Proving","author":"F Immler","year":"2016","unstructured":"Immler, F., Traut, C.: The flow of ODEs. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 184\u2013199. Springer, Cham (2016). doi:10.1007\/978-3-319-43144-4_12"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: $$\\delta $$-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200\u2013205. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_15"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1) (2011)","DOI":"10.2168\/LMCS-9(1:1)2013"},{"key":"14_CR20","unstructured":"The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project (2004). http:\/\/coq.inria.fr, version 8.0"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Mitsch, S., Platzer, A.: The KeYmaera X proof IDE: concepts on usability in hybrid systems theorem proving. In: FIDE-3. EPTCS, vol. 240, pp. 67\u201381 (2016)","DOI":"10.4204\/EPTCS.240.5"},{"issue":"1","key":"14_CR22","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. Form. Methods Syst. Des. 49(1), 33\u201374 (2016). Special issue of selected papers from RV\u201914","journal-title":"Form. Methods Syst. Des."},{"key":"14_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). doi:10.1007\/3-540-45949-9"},{"issue":"2","key":"14_CR24","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. Reason. 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reason."},{"key":"14_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14509-4"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logics of dynamical systems. In: LICS. pp. 13\u201324. IEEE (2012)","DOI":"10.1109\/LICS.2012.13"},{"issue":"2","key":"14_CR27","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2017","unstructured":"Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219\u2013266 (2017)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"14_CR28","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. Form. Methods Syst. Des. 35(1), 98\u2013120 (2009). Special issue for selected papers from CAV\u201908","journal-title":"Form. Methods Syst. Des."},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","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, vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-71070-7_15"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","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, vol. 5663, pp. 485\u2013501. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02959-2_35"},{"key":"14_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-38088-4_26","volume-title":"NASA Formal Methods","author":"A Solovyev","year":"2013","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 383\u2013397. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38088-4_26"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:06:32Z","timestamp":1664431592000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}