{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T03:54:24Z","timestamp":1772078064762,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642134630","type":"print"},{"value":"9783642134647","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13464-7_13","type":"book-chapter","created":{"date-parts":[[2010,6,7]],"date-time":"2010-06-07T10:50:49Z","timestamp":1275907849000},"page":"155-169","source":"Crossref","is-referenced-by-count":10,"title":["Model Checking of Hybrid Systems Using Shallow Synchronization"],"prefix":"10.1007","author":[{"given":"Lei","family":"Bu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Mover","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"13_CR1","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1145\/1132357.1132363","volume":"5","author":"R. Alur","year":"2006","unstructured":"Alur, R., Dang, T., Ivancic, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embedded Comput. Syst.\u00a05(1), 152\u2013199 (2006)","journal-title":"ACM Trans. Embedded Comput. Syst."},{"issue":"2","key":"13_CR2","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.entcs.2004.12.022","volume":"119","author":"G. Audemard","year":"2005","unstructured":"Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying Industrial Hybrid Systems with MathSAT. Electr. Notes Theor. Comput. Sci.\u00a0119(2), 17\u201332 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/BFb0055643","volume-title":"CONCUR \u201998 Concurrency Theory","author":"J. Bengtsson","year":"1998","unstructured":"Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial Order Reductions for Timed Systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 485\u2013500. Springer, Heidelberg (1998)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"13_CR5","unstructured":"Bu, L., Li, X.: Path-Oriented Bounded Reachability Analysis of Compositional Linear Hybrid Systems. Manuscript submitted (2008)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Bu, L., Li, Y., Wang, L., Chen, X., Li, X.: BACH2: Bounded reachAbility CHecker for Compositional Linear Hybrid Systems. In: DATE, pp. 1512\u20131517. EDAA (2010)","DOI":"10.1109\/DATE.2010.5457051"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.entcs.2004.08.061","volume":"133","author":"M. Fr\u00e4nzle","year":"2005","unstructured":"Fr\u00e4nzle, M., Herde, C.: Efficient Proof Engines for Bounded Model Checking of Hybrid Systems. Electr. Notes Theor. Comput. Sci.\u00a0133, 119\u2013137 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"3","key":"13_CR9","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design\u00a030(3), 179\u2013198 (2007)","journal-title":"Formal Methods in System Design"},{"key":"13_CR10","first-page":"672","volume-title":"DAC","author":"N. Giorgetti","year":"2005","unstructured":"Giorgetti, N., Pappas, G.J., Bemporad, A.: Bounded model checking for hybrid dynamical systems. In: DAC, pp. 672\u2013677. IEEE, Los Alamitos (2005)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. In: Godefroid, P. (ed.) Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"issue":"4-5","key":"13_CR12","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1017\/S1471068403001790","volume":"3","author":"K. Heljanko","year":"2003","unstructured":"Heljanko, K., Niemel\u00e4, I.: Bounded LTL model checking with stable models. Theory and Practice of Logic Programming\u00a03(4-5), 519\u2013550 (2003)","journal-title":"Theory and Practice of Logic Programming"},{"key":"13_CR13","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":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-71493-4_24","volume-title":"Hybrid Systems: Computation and Control","author":"S. Jha","year":"2007","unstructured":"Jha, S., Krogh, B., Weimer, J., Clarke, E.: Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 287\u2013300. Springer, Heidelberg (2007)"},{"issue":"3-4","key":"13_CR15","first-page":"141","volume":"3","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisability modulo theories. JSAT\u00a03(3-4), 141\u2013224 (2007)","journal-title":"JSAT"},{"key":"13_CR16","first-page":"1","volume-title":"EMSOFT","author":"U. Shinya","year":"2008","unstructured":"Shinya, U.: Event order abstraction for parametric real-time system verification. In: EMSOFT, pp. 1\u201310. ACM, New York (2008)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-78800-3_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Wang","year":"2008","unstructured":"Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole Partial Order Reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 382\u2013396. Springer, Heidelberg (2008)"},{"issue":"1","key":"13_CR18","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/TSE.2005.13","volume":"31","author":"F. Wang","year":"2005","unstructured":"Wang, F.: Symbolic parametric safety analysis of linear hybrid systems with BDD-like data structures. IEEE Trans. Soft. Eng.\u00a031(1), 38\u201351 (2005)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","first-page":"34","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J. Zhao","year":"2004","unstructured":"Zhao, J., Li, X., Zheng, T., Zheng, G.: Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 34\u201345. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13464-7_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T18:35:40Z","timestamp":1740162940000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13464-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642134630","9783642134647"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13464-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}