{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:40:41Z","timestamp":1780116041304,"version":"3.54.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,2,28]],"date-time":"2015-02-28T00:00:00Z","timestamp":1425081600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10703-015-0225-4","type":"journal-article","created":{"date-parts":[[2015,2,27]],"date-time":"2015-02-27T07:27:15Z","timestamp":1425022035000},"page":"105-134","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Hybrid automata-based CEGAR for rectangular hybrid systems"],"prefix":"10.1007","volume":"46","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","published-online":{"date-parts":[[2015,2,28]]},"reference":[{"key":"225_CR1","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification, vol 1855 of Lecture Notes in Computer Science. pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"225_CR2","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani S (2000) Bebop: a symbolic model checker for Boolean programs. In: Proceedings of the 7th international SPIN, pp 113\u2013130","DOI":"10.1007\/10722468_7"},{"key":"225_CR3","doi-asserted-by":"crossref","unstructured":"Corbett J, Dwyer M, Hatcliff J, Laubach S, Robby C. Pasareanu, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: Proceedings of ICSE. pp 439\u2013448","DOI":"10.1145\/337180.337234"},{"key":"225_CR4","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy Abstraction. In: Proceedings of 29th ACM symposium on principles of programming languages (POPL\u201902). pp 58\u201370","DOI":"10.1145\/503272.503279"},{"issue":"2","key":"225_CR5","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1002\/bltj.2223","volume":"5","author":"G Holzmann","year":"2000","unstructured":"Holzmann G, Smith M (2000) Automating software feature verification. Bell Labs Tech J 5(2):72\u201387","journal-title":"Bell Labs Tech J"},{"key":"225_CR6","doi-asserted-by":"crossref","unstructured":"Alur R, Dang T, Ivancic F (2003) Counter-example guided predicate abstraction of hybrid systems. In: Proceedings of TACAS 2003. pp 208\u2013223","DOI":"10.1007\/3-540-36577-X_15"},{"issue":"4","key":"225_CR7","first-page":"583","volume":"14","author":"EM Clarke","year":"2003","unstructured":"Clarke EM, Fehnker A, Han Z, Krogh B, Ouaknine J, Stursberg O, Theobald M (2003) Abstraction and counterexample-guided refinement in model checking of hybrid systems. JFCS 14(4):583\u2013604","journal-title":"JFCS"},{"key":"225_CR8","unstructured":"Clarke E.M., Fehnker A, Han Z, Krogh B, Ouaknine J, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexmple-guided abstraction refinement. In: Proceedings of TACAS. pp 192\u2013207"},{"key":"225_CR9","doi-asserted-by":"crossref","unstructured":"Dierks H, Kupferschmid S, Larsen KG (2007) Automatic Abstraction refinement for timed automata. In: Proceedings of FORMATS. pp 114\u2013129","DOI":"10.1007\/978-3-540-75454-1_10"},{"key":"225_CR10","doi-asserted-by":"crossref","unstructured":"Fehnker A, Clarke EM, Jha S, Krogh B (2005) Refining abstractions of hybrid systems using counterexample fragments. In: Proceedings of HSCC 2005. pp 242\u2013257","DOI":"10.1007\/978-3-540-31954-2_16"},{"key":"225_CR11","unstructured":"Segelken M (2007) Abstraction and Counterexample-guided construction of omega-automata for model checking of step-discrete linear hybrid models. In: Proceedings of CAV. pp 433\u2013448"},{"key":"225_CR12","doi-asserted-by":"crossref","unstructured":"Sorea M (2004) Lazy approximation for dense real-time systems. In: Proceedings of FORMATS\/FTRFTS. pp 363\u2013378","DOI":"10.1007\/978-3-540-30206-3_25"},{"key":"225_CR13","doi-asserted-by":"crossref","unstructured":"Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8","DOI":"10.1145\/1210268.1210276"},{"key":"225_CR14","unstructured":"Graf S, Saidi H (1997) Construction of abstact state graphs with PVS. In: Proceedings of CAV, pp 72\u201383"},{"key":"225_CR15","doi-asserted-by":"crossref","unstructured":"Jha SK, Krogh BH, Weimer JE, Clarke EM (2007) Reachability for linear hybrid automata using iterative relaxation abstraction. In: Proceedings of HSCC 2007, pp 287\u2013300","DOI":"10.1007\/978-3-540-71493-4_24"},{"key":"225_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger TA (1996) The theory of hybrid automata. In: LICS, pp 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"key":"225_CR17","unstructured":"Hybrid abstraction refinement engine (HARE) (2013). In: http:\/\/publish.illinois.edu\/hare-tool\/"},{"key":"225_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Ho P-H, Howard W-T (1997) Hytech: a model checker for hybrid systems. In: Proceedings of CAV. pp 460\u2013483","DOI":"10.1007\/3-540-63166-6_48"},{"key":"225_CR19","doi-asserted-by":"crossref","unstructured":"Frehse G (2005) Phaver: algorithmic verification of hybrid systems past hytech. In: Proceedings of HSCC. pp 258\u2013273","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"225_CR20","doi-asserted-by":"crossref","unstructured":"Frehse G, Le Guernic C, Donz\u00e9 A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In Proceedings of CAV","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"225_CR21","doi-asserted-by":"crossref","unstructured":"Asarin E, Dang T, Maler O (2002) The d\/dt tool for verification of hybrid system","DOI":"10.1007\/3-540-45657-0_30"},{"key":"225_CR22","doi-asserted-by":"crossref","unstructured":"Prabhakar P, Duggirala PS, Mitra S, Viswanathan M (2013) Hybrid automata-based cegar for rectangular hybrid systems. In: Proceedings of VMCAI. pp 48\u201367","DOI":"10.1007\/978-3-642-35873-9_6"},{"key":"225_CR23","doi-asserted-by":"crossref","unstructured":"Doyen L, Henzinger TA, Raskin J-F (2005) Automatic rectangular refinement of affine hybrid systems. In: Proceedings of FORMATS05, vol 3829 in LNCS. pp 144\u2013161","DOI":"10.1007\/11603009_13"},{"key":"225_CR24","unstructured":"Henzinger TA, Kopke PW, Puri A, Varaiya P (1995) What\u2019s decidable about hybrid automata? In: Proceedings of STOC. pp 373\u2013382"},{"issue":"1","key":"225_CR25","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"Rajeev Alur","year":"1995","unstructured":"Alur Rajeev, Courcoubetis Costas, Halbwachs Nicolas, Henzinger Thomas A, Ho P-H, Nicollin Xavier, Olivero Alfredo, Sifakis Joseph, Yovine Sergio (1995) The algorithmic analysis of hybrid systems. TCS 138(1):3\u201334","journal-title":"TCS"},{"key":"225_CR26","doi-asserted-by":"crossref","unstructured":"Fehnker A, Ivancic F (2004) Benchmarks for hybrid systems verification. pp 326\u2013341","DOI":"10.1007\/978-3-540-24743-2_22"},{"key":"225_CR27","doi-asserted-by":"crossref","unstructured":"Munoz CA, Dowek G, Carreo V (2004) Modeling and verification of an air traffic concept of operations. In: ISSTA, pp 175\u2013182","DOI":"10.1145\/1007512.1007536"},{"key":"225_CR28","unstructured":"Dutertre B, Sorea M (2004) Timed systems in SAL. Technical report, Computer Science Laboratory"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0225-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0225-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0225-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,7]],"date-time":"2024-06-07T12:51:54Z","timestamp":1717764714000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0225-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,28]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["225"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0225-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,28]]}}}