{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:32:00Z","timestamp":1777890720395,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540710691","type":"print"},{"value":"9783540710707","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_15","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"171-178","source":"Crossref","is-referenced-by-count":148,"title":["KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)"],"prefix":"10.1007","author":[{"given":"Andr\u00e9","family":"Platzer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan-David","family":"Quesel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","first-page":"48","volume-title":"ICECCS","author":"E. \u00c1brah\u00e1m-Mumm","year":"2001","unstructured":"\u00c1brah\u00e1m-Mumm, E., Steffen, M., Hannemann, U.: Verification of hybrid systems: Formalization and proof rules in PVS. In: ICECCS, pp. 48\u201357. IEEE Computer, Los Alamitos (2001)"},{"key":"15_CR2","series-title":"Lecture Notes in Artificial Intelligence","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.\u00a04334. Springer, Heidelberg (2007)"},{"issue":"3","key":"15_CR3","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G.E. Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput.\u00a012(3), 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Davoren, J.M., Nerode, A.: Logics for hybrid systems. IEEE 88(7) (July 2000)","DOI":"10.1109\/5.871305"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"15_CR6","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. MIT Press, Cambridge (2000)"},{"key":"15_CR7","first-page":"278","volume-title":"LICS","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278\u2013292. IEEE Computer Society, Los Alamitos (1996)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Hybrid Systems: Computation and Control","author":"Z. Manna","year":"1998","unstructured":"Manna, Z., Sipma, H.: Deductive verification of hybrid systems using STeP. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol.\u00a01386. Springer, Heidelberg (1998)"},{"key":"15_CR9","volume-title":"FLAIRS","author":"A. Nonnengart","year":"2001","unstructured":"Nonnengart, A., Rock, G., Stephan, W.: Using hybrid automata to express realtime properties in VSE-II. In: Russell, I., Kolen, J.F. (eds.) FLAIRS. AAAI Press, Menlo Park (2001)"},{"key":"15_CR10","unstructured":"Platzer, A.: Combining deduction and algebraic constraints for hybrid system analysis. In: Beckert, B. (ed.) VERIFY 2007 at CADE 2007, CEUR-WS.org (2007)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Differential algebraic dynamic logic for differential algebraic programs. (submitted, 2007)","DOI":"10.1093\/logcom\/exn070"},{"key":"15_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-73099-6_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Platzer","year":"2007","unstructured":"Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol.\u00a04548, pp. 216\u2013232. Springer, Heidelberg (2007)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning (to appear, 2008)","DOI":"10.1007\/s10817-008-9103-8"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"HSCC","author":"A. Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.D.: Logical verification and systematic parametric analysis in train control. In: Egerstedt, M., Mishra, B. (eds.) HSCC. LNCS, Springer, Heidelberg (2008)"},{"key":"15_CR15","unstructured":"Silva, B.I., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verification of hybrid dynamical system using CheckMate. In: ADPM 2000: 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems (2000)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: a study in multi-agent hybrid systems. IEEE T. Automat. Contr. 43(4) (1998)","DOI":"10.1109\/9.664154"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:15:09Z","timestamp":1605762909000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}