{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:15:00Z","timestamp":1771485300467,"version":"3.50.1"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_36","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"527-538","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":160,"title":["KeYmaera\u00a0X: An Axiomatic Tactical Theorem Prover for Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Nathan","family":"Fulton","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[]},{"given":"Jan-David","family":"Quesel","sequence":"additional","affiliation":[]},{"given":"Marcus","family":"V\u00f6lp","sequence":"additional","affiliation":[]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"issue":"1","key":"36_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Softw. Syst. Model. 4(1), 32\u201354 (2005)","journal-title":"Softw. Syst. Model."},{"key":"36_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","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., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993)"},{"key":"36_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","first-page":"453","volume-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334, pp. 453\u2013479. Springer, Heidelberg (2007)"},{"issue":"4","key":"36_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1049\/sej.1993.0025","volume":"8","author":"J Bowen","year":"1993","unstructured":"Bowen, J., Stavridou, V.: Safety-critical systems, formal methods and standards. Softw. Eng. J. 8(4), 189\u2013209 (1993)","journal-title":"Softw. Eng. J."},{"key":"36_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/3-540-58156-1_44","volume-title":"Automated Deduction - CADE-12","author":"A Felty","year":"1994","unstructured":"Felty, A., Howe, D.: Tactic theorem proving with refinement-tree proofs and metavariables. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 605\u2013619. Springer, Heidelberg (1994)"},{"key":"36_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-52885-7_83","volume-title":"10th International Conference on Automated Deduction","author":"M Heisel","year":"1990","unstructured":"Heisel, M., Reif, W., Stephan, W.: Tactical theorem proving in program verification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 117\u2013131. Springer, Heidelberg (1990)"},{"key":"36_CR7","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal project, version 8.0 (2004). http:\/\/coq.inria.fr"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-319-11164-3_17","volume-title":"Runtime Verification","author":"S Mitsch","year":"2014","unstructured":"Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 199\u2013214. Springer, Heidelberg (2014)"},{"key":"36_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"issue":"2","key":"36_CR10","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. Reas. 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reas."},{"key":"36_CR11","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)"},{"key":"36_CR12","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logics of Dynamical Systems. In: LICS, pp. 13\u201324. IEEE (2012)","DOI":"10.1109\/LICS.2012.13"},{"key":"36_CR13","unstructured":"Platzer, A.: Differential Game Logic. CoRR abs\/1408.1980 (2014)"},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"Platzer, A.: A uniform substitution calculus for differential dynamic logic. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. xx\u2013yy. Springer, Heidelberg (2015)","DOI":"10.1007\/978-3-319-21401-6_32"},{"key":"36_CR15","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)"},{"key":"36_CR16","doi-asserted-by":"crossref","unstructured":"Quesel, J.D., Mitsch, S., Loos, S., Ar\u00e9chiga, N., Platzer, A.: How to model and prove hybrid systems with KeYmaera: a tutorial on safety. STTT (2015)","DOI":"10.1007\/s10009-015-0367-0"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T09:46:49Z","timestamp":1676972809000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}