{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T10:11:20Z","timestamp":1781086280854,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540730989","type":"print"},{"value":"9783540730996","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73099-6_17","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T07:04:02Z","timestamp":1189753442000},"page":"216-232","source":"Crossref","is-referenced-by-count":32,"title":["Differential Dynamic Logic for Verifying Parametric Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Andr\u00e9","family":"Platzer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"17_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems. IEEE Trans. Software Eng.\u00a022(3), 181\u2013201 (1996)","journal-title":"IEEE Trans. Software Eng."},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-45351-2_9","volume-title":"Hybrid Systems: Computation and Control","author":"H. Anai","year":"2001","unstructured":"Anai, H., Weispfenning, V.: Reach set computations using real quantifier elimination. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 63\u201376. Springer, Heidelberg (2001)"},{"key":"17_CR3","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"17_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11814771_23","volume-title":"Automated Reasoning","author":"B. Beckert","year":"2006","unstructured":"Beckert, B., Platzer, A.: Dynamic logic with non-rigid functions: A basis for object-oriented program verification. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 266\u2013280. Springer, Heidelberg (2006)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-71493-4","volume-title":"HSCC 2007","author":"A. Bemporad","year":"2007","unstructured":"Bemporad, A., Bicchi, A., Buttazzo, G.: Hybrid Systems: Computation and Control. In: HSCC 2007. 10th International Conference, Pisa, Italy. LNCS, vol.\u00a04416, Springer, Heidelberg (2007)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-36580-X_11","volume-title":"Hybrid Systems: Computation and Control","author":"R.J. Boulton","year":"2003","unstructured":"Boulton, R.J., Hardy, R., Martin, U.: A Hoare logic for single-input single-output continuous-time control systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 113\u2013125. Springer, Heidelberg (2003)"},{"key":"17_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"3","key":"17_CR8","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":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/978-3-540-30101-1_4","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2004","unstructured":"Damm, W., Hungar, H., Olderog, E.-R.: On the verification of cooperating traffic agents. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol.\u00a03188, pp. 77\u2013110. Springer, Heidelberg (2004)"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-49163-5_3","volume-title":"Hybrid Systems V","author":"J.M. Davoren","year":"1999","unstructured":"Davoren, J.M.: On hybrid systems and the modal \u03bc-calculus. In: Antsaklis, P.J., Kohn, W., Lemmon, M.D., Nerode, A., Sastry, S.S. (eds.) Hybrid Systems V. LNCS, vol.\u00a01567, pp. 38\u201369. Springer, Heidelberg (1999)"},{"issue":"7","key":"17_CR11","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1109\/5.871305","volume":"88","author":"J.M. Davoren","year":"2000","unstructured":"Davoren, J.M., Nerode, A.: Logics for hybrid systems. Proceedings of the IEEE\u00a088(7), 985\u20131010 (2000)","journal-title":"Proceedings of the IEEE"},{"key":"17_CR12","first-page":"76","volume-title":"FMCAD","author":"J. Faber","year":"2006","unstructured":"Faber, J., Meyer, R.: Model checking data-dependent real-time properties of the European Train Control System. In: FMCAD, pp. 76\u201377. IEEE Computer Society, Washington (2006)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-48168-0_10","volume-title":"Computer Science Logic","author":"M. Fr\u00e4nzle","year":"1999","unstructured":"Fr\u00e4nzle, M.: Analysis of hybrid systems. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 126\u2013140. Springer, Heidelberg (1999)"},{"key":"17_CR14","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":"17_CR15","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":"17_CR16","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, Washington (1996)"},{"key":"17_CR17","first-page":"394","volume-title":"LICS","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: LICS, pp. 394\u2013406. IEEE Computer Society, Washington (1992)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Langenstein, B., Sengler, C., Siekmann, J.H., Stephan, W., Wolpers, A.: Deduction in the verification support environment (VSE). In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, Springer, Heidelberg (1996)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-48983-5_15","volume-title":"Hybrid Systems: Computation and Control","author":"G. Lafferriere","year":"1999","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569, pp. 137\u2013151. Springer, Heidelberg (1999)"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/11513988_3","volume-title":"Computer Aided Verification","author":"C. Piazza","year":"2005","unstructured":"Piazza, C., Antoniotti, M., Mysore, V., Policriti, A., Winkler, F., Mishra, B.: Algorithmic algebraic model checking I. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 5\u201319. Springer, Heidelberg (2005)"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Differential logic for reasoning about hybrid systems. In: Bemporad et al. [5] p. 746\u2013749","DOI":"10.1007\/978-3-540-71493-4_75"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/978-3-540-72734-7_32","volume-title":"LFCS 2007","author":"A. Platzer","year":"2007","unstructured":"Platzer, A.: A temporal dynamic logic for verifying hybrid system invariants. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. Logical Foundations of Computer Science, International Symposium, New York, USA. LNCS, vol.\u00a04514, pp. 457\u2013471. Springer, Heidelberg (2007)"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Towards a hybrid dynamic logic for hybrid dynamic systems. In: Blackburn, P., Bolander, T., Bra\u00fcner, T., de\u00a0Paiva, V., Villadsen, J. (eds.), Proc. LICS International Workshop on Hybrid Logic, 2006, Seattle, ENTCS (2007)","DOI":"10.1016\/j.entcs.2006.11.026"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad et\u00a0al. [5] p. 473\u2013486","DOI":"10.1007\/978-3-540-71493-4_37"},{"issue":"1","key":"17_CR25","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1016\/S0304-3975(02)00547-9","volume":"290","author":"M. R\u00f6nkk\u00f6","year":"2003","unstructured":"R\u00f6nkk\u00f6, M., Ravn, A.P., Sere, K.: Hybrid action systems. Theor. Comput. Sci.\u00a0290(1), 937\u2013973 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"508","DOI":"10.1007\/978-3-540-24743-2_34","volume-title":"Hybrid Systems: Computation and Control","author":"W.C. Rounds","year":"2004","unstructured":"Rounds, W.C.: A spatial logic for the hybrid \u03c0-calculus. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 508\u2013522. Springer, Heidelberg (2004)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","first-page":"36","volume-title":"Hybrid Systems","author":"C. Zhou","year":"1993","unstructured":"Zhou, C., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) Hybrid Systems. LNCS, vol.\u00a0736, pp. 36\u201359. Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73099-6_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:59Z","timestamp":1619517599000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73099-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730989","9783540730996"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73099-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}