{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T21:31:14Z","timestamp":1760131874723,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_22","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"276-291","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Verification of Hybrid Systems with Large Discrete State Space"],"prefix":"10.1007","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Disch","sequence":"additional","affiliation":[]},{"given":"Hardi","family":"Hungar","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Pigorsch","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]},{"given":"Boris","family":"Wirtz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E. Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of the hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 365\u2013370. Springer, Heidelberg (2002)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/3-540-48092-7_14","volume-title":"Correct System Design","author":"T. Bienm\u00fcller","year":"1999","unstructured":"Bienm\u00fcller, T., Bohn, J., Brinkmann, H., Brockmeyer, U., Damm, W., Hungar, H., Jansen, P.: Verification of the automotive control units. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol.\u00a01710, pp. 319\u2013341. Springer, Heidelberg (1999)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-49382-2_27","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"J. Bohn","year":"1998","unstructured":"Bohn, J., Damm, W., Grumberg, O., Hungar, H., Laster, K.: First-order-CTL model checking. In: Arvind, V., Ramanujam, R. (eds.) FST TCS 1998. LNCS, vol.\u00a01530, pp. 283\u2013294. Springer, Heidelberg (1998)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Bretschneider, M., Holberg, H.-J., B\u00f6de, E., Br\u00fcckner, I., Peikenkamp, T., Spenke, H.: Model-based safety analysis of a flap control system. In: Proc. 14th Annual INCOSE Symposium (2004)","DOI":"10.1002\/j.2334-5837.2004.tb00493.x"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. In: Proc. LICS 1990, pp. 428\u2013439 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proc. IEEE CDC 1998 (1998)","DOI":"10.1109\/CDC.1998.758642"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-48983-5_10","volume-title":"Hybrid Systems: Computation and Control","author":"A. Chutinan","year":"1999","unstructured":"Chutinan, A., Krogh, B.H.: Verification of the polyhedral-invariant hybrid automata using polygonal flowpipe approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569, pp. 76\u201390. Springer, Heidelberg (1999)"},{"issue":"4","key":"22_CR8","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Foundations of Computer Science\u00a014(4), 583\u2013604 (2003)","journal-title":"Foundations of Computer Science"},{"key":"22_CR9","first-page":"119","volume":"133","author":"M. Fr\u00e4nzle","year":"2005","unstructured":"Fr\u00e4nzle, M., Herde, C.: Efficient proof engines for bounded model checking of hybrid systems. ENTCS\u00a0133, 119\u2013137 (2005)","journal-title":"ENTCS"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"22_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proc. LICS 1996, pp. 278\u2013292 (1996)","DOI":"10.1109\/LICS.1996.561342"},{"issue":"1-2","key":"22_CR12","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer\u00a01(1-2), 110\u2013122 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"22_CR13","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communication of the ACM\u00a012, 576\u2013583 (1969)","journal-title":"Communication of the ACM"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Correct Hardware Design and Verification Methods","author":"H. Hungar","year":"1995","unstructured":"Hungar, H., Grumberg, O., Damm, W.: What if model checking must be truly symbolic. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 1\u201320. Springer, Heidelberg (1995)"},{"key":"22_CR15","unstructured":"Mishchenko, A., Chatterjee, S., Jiang, R., Brayton, R.K.: FRAIGs: A unifying representation for logic synthesis and verification. Technical report, EECS Dept., UC Berkeley (2005)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Pigorsch, F., Scholl, C., Disch, S.: Advanced unbounded model checking by using AIGs, BDD sweeping and quantifier scheduling. In: Proc. FMCAD 2006 (2006)","DOI":"10.1109\/FMCAD.2006.4"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Silva, B.I., Krogh, B.H.: Modeling and verification of hybrid system with clocked and unclocked events. In: Proc. IEEE CDC 2001 (2001)","DOI":"10.1109\/CDC.2001.980198"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Silva, B.I., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verification of hybrid dynamical system using CheckMate. In: Proc. 4th Conference on Automation of Mixed Processes (2000)","DOI":"10.1109\/ACC.2000.879487"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control","author":"A. Tiwari","year":"2002","unstructured":"Tiwari, A., Khanna, G.: Series of the abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol.\u00a02289, pp. 465\u2013478. Springer, Heidelberg (2002)"},{"issue":"2","key":"22_CR21","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1109\/TCST.2004.824309","volume":"12","author":"F.D. Torrisi","year":"2004","unstructured":"Torrisi, F.D., Bemporad, A.: HYSDEL - A tool for generating computational hybrid models. IEEE Transactions on Control Systems Technology\u00a012(2), 235\u2013249 (2004)","journal-title":"IEEE Transactions on Control Systems Technology"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T09:47:37Z","timestamp":1736588857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11901914_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}