{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:13Z","timestamp":1725494413376},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_11","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T07:58:07Z","timestamp":1194854287000},"page":"151-166","source":"Crossref","is-referenced-by-count":1,"title":["Language-Based Abstraction Refinement for Hybrid System Verification"],"prefix":"10.1007","author":[{"given":"Felix","family":"Klaedtke","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Ratschan","sequence":"additional","affiliation":[]},{"given":"Zhikun","family":"She","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"11_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., Ivan\u010di\u0107, 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."},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-45351-2_11","volume-title":"Hybrid Systems: Computation and Control","author":"E. Asarin","year":"2001","unstructured":"Asarin, E., Schneider, G., Yovine, S.: On the decidability of the reachability problem for planar differential inclusions. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 89\u2013104. Springer, Heidelberg (2001)"},{"issue":"4","key":"11_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1016\/j.jco.2004.09.003","volume":"21","author":"T. Brihaye","year":"2005","unstructured":"Brihaye, T., Michaux, C.: On the expressiveness and decidability of o-minimal hybrid systems. J. Complexity\u00a021(4), 447\u2013478 (2005)","journal-title":"J. Complexity"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-3-540-24743-2_15","volume-title":"Hybrid Systems: Computation and Control","author":"T. Brihaye","year":"2004","unstructured":"Brihaye, T., et al.: On o-minimal hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 219\u2013233. Springer, Heidelberg (2004)"},{"issue":"4","key":"11_CR5","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., et al.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Internat. J. Found. Comput. Sci.\u00a014(4), 583\u2013604 (2003)","journal-title":"Internat. J. Found. Comput. Sci."},{"issue":"5","key":"11_CR6","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., et al.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Dams, D.: Comparing abstraction refinement algorithms. In: Proc. of 2nd Workshop on Software Model Checking (SoftMC\u201903), Electr. Notes Theor. Comput. Sci. 89(3), 405\u2013416 (2003)","DOI":"10.1016\/S1571-0661(05)80003-9"},{"issue":"3","key":"11_CR8","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0004-3702(87)90091-9","volume":"32","author":"E. Davis","year":"1987","unstructured":"Davis, E.: Constraint propagation with interval labels. Artif. Intell.\u00a032(3), 281\u2013331 (1987)","journal-title":"Artif. Intell."},{"key":"11_CR9","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":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., et al.: 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":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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: An ounce of realism can save an infinity of states. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 126\u2013140. Springer, Heidelberg (1999)"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., et al.: What\u2019s decidable about hybrid automata. J. Comput. System Sci.\u00a057, 94\u2013124 (1998)","journal-title":"J. Comput. System Sci."},{"issue":"4","key":"11_CR13","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N. Klarlund","year":"2002","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. Internat. J. Found. Comput. Sci.\u00a013(4), 571\u2013586 (2002)","journal-title":"Internat. J. Found. Comput. Sci."},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11730637_27","volume-title":"Hybrid Systems: Computation and Control","author":"M. Kloetzer","year":"2006","unstructured":"Kloetzer, M., Belta, C.: Reachability analysis of multi-affine systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol.\u00a03927, pp. 348\u2013362. Springer, Heidelberg (2006)"},{"key":"11_CR15","unstructured":"Ratschan, S.: RSolver. \n                    \n                      http:\/\/rsolver.sourceforge.net\n                    \n                    \n                  . Software package"},{"key":"11_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-45470-5_18","volume-title":"Artificial Intelligence, Automated Reasoning, and Symbolic Computation","author":"S. Ratschan","year":"2002","unstructured":"Ratschan, S.: Continuous first-order constraint satisfaction. In: Calmet, J., et al. (eds.) AISC 2002 and Calculemus 2002. LNCS (LNAI), vol.\u00a02385, pp. 181\u2013195. Springer, Heidelberg (2002)"},{"key":"11_CR17","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans. Embedded Comput. Syst. (to appear)"},{"key":"11_CR18","unstructured":"Ratschan, S., She, Z.: HSolver, \n                    \n                      http:\/\/hsolver.sourceforge.net\n                    \n                    \n                  . Software package"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/978-3-540-31954-2_37","volume-title":"Hybrid Systems: Computation and Control","author":"S. Ratschan","year":"2005","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 573\u2013589. Springer, Heidelberg (2005)"},{"key":"11_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/11856290_18","volume-title":"Artificial Intelligence and Symbolic Computation","author":"S. Ratschan","year":"2006","unstructured":"Ratschan, S., She, Z.: Constraints for continuous reachability in the verification of hybrid systems. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol.\u00a04120, pp. 196\u2013210. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:45:02Z","timestamp":1620002702000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_11","relation":{},"subject":[]}}