{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T21:39:41Z","timestamp":1791236381876,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642358722","type":"print"},{"value":"9783642358739","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35873-9_6","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T06:22:57Z","timestamp":1357107777000},"page":"48-67","source":"Crossref","is-referenced-by-count":19,"title":["Hybrid Automata-Based CEGAR for Rectangular Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Pavithra","family":"Prabhakar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Parasara Sridhar","family":"Duggirala","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"HARE, https:\/\/wiki.cites.uiuc.edu\/wiki\/display\/MitraResearch\/HARE"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-36577-X_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2003","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Counter-Example Guided Predicate Abstraction of Hybrid Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 208\u2013223. Springer, Heidelberg (2003)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of hybrid system (2002)","DOI":"10.1007\/3-540-45657-0_30"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.: Bebop: A Symbolic Model Checker for Boolean Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"issue":"4","key":"6_CR5","first-page":"583","volume":"14","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. JFCS\u00a014(4), 583\u2013604 (2003)","journal-title":"JFCS"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-36577-X_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B., Stursberg, O., Theobald, M.: Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 192\u2013207. Springer, Heidelberg (2003)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: ICSE, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-75454-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H. Dierks","year":"2007","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic Abstraction Refinement for Timed Automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 114\u2013129. Springer, Heidelberg (2007)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/11603009_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"L. Doyen","year":"2005","unstructured":"Doyen, L., Henzinger, T.A., Raskin, J.-F.: Automatic Rectangular Refinement of Affine Hybrid Systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol.\u00a03829, pp. 144\u2013161. Springer, Heidelberg (2005)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-540-31954-2_16","volume-title":"Hybrid Systems: Computation and Control","author":"A. Fehnker","year":"2005","unstructured":"Fehnker, A., Clarke, E.M., Jha, S., Krogh, B.: Refining Abstractions of Hybrid Systems Using Counterexample Fragments. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 242\u2013257. Springer, Heidelberg (2005)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"6_CR13","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":"6_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: POPL 2002, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In: Proc. of STOC, pp. 373\u2013382 (1995)","DOI":"10.1145\/225058.225162"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278\u2013292 (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: A Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 460\u2013483. Springer, Heidelberg (1997)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Howard, W.-T.: Hytech: A Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 460\u2013483. Springer, Heidelberg (1997)"},{"issue":"2","key":"6_CR19","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1002\/bltj.2223","volume":"5","author":"G. Holzmann","year":"2000","unstructured":"Holzmann, G., Smith, M.: Automating software feature verification. Bell Labs Technical Journal\u00a05(2), 72\u201387 (2000)","journal-title":"Bell Labs Technical Journal"},{"key":"6_CR20","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.K. Jha","year":"2007","unstructured":"Jha, S.K., Krogh, B.H., Weimer, J.E., Clarke, E.M.: 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)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Munoz, C.A., Dowek, G., Carreo, V.: Modeling and verification of an air traffic concept of operations. In: ISSTA, pp. 175\u2013182 (2004)","DOI":"10.1145\/1013886.1007536"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Prabhakar, P., Duggirala, S., Mitra, S., Viswanathan, M.: Hybrid automata-based cegar for rectangular hybrid automata, http:\/\/software.imdea.org\/people\/pavithra.prabhakar\/Papers\/vmcai2013tr.pdf","DOI":"10.1007\/978-3-642-35873-9_6"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-73368-3_46","volume-title":"Computer Aided Verification","author":"M. Segelken","year":"2007","unstructured":"Segelken, M.: Abstraction and Counterexample-Guided Construction of \u03c9-Automata for Model Checking of Step-Discrete Linear Hybrid Models. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 433\u2013448. Springer, Heidelberg (2007)"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-30206-3_25","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"M. Sorea","year":"2004","unstructured":"Sorea, M.: Lazy Approximation for Dense Real-Time Systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRFTS 2004. LNCS, vol.\u00a03253, pp. 363\u2013378. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35873-9_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T15:33:43Z","timestamp":1745940823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35873-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642358722","9783642358739"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35873-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}