{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:20:18Z","timestamp":1761488418836},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-36577-x_15","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"208-223","source":"Crossref","is-referenced-by-count":52,"title":["Counter-Example Guided Predicate Abstraction of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Thao","family":"Dang","sequence":"additional","affiliation":[]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3\u201334, 1995.","journal-title":"Theoretical Computer Science"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, T. Dang, J. Esposito, Y. Hur, F. Ivan\u010di\u0107, V. Kumar, I. Lee, P. Mishra, G. Pappas, and O. Sokolsky. Hierarchical modeling and analysis of embedded systems. Proceedings of the IEEE, 91(1), January 2003.","DOI":"10.1109\/JPROC.2002.805817"},{"key":"15_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Reachability analysis of hybrid systems via predicate abstraction","author":"R. Alur","year":"2002","unstructured":"R. Alur, T. Dang, and F. Iva\u010di\u0107. Reachability analysis of hybrid systems via predicate abstraction. In Hybrid Systems: Computation and Control, Fifth International Workshop, LNCS 2289. Springer-Verlag, 2002."},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1006\/inco.1995.1059","volume":"118","author":"R. Alur","year":"1995","unstructured":"R. Alur, A. Itai, R.P. Kurshan, and M. Yannakakis. Timing verification by successive approximation. Information and Computation, 118(1):142\u2013157, 1995.","journal-title":"Information and Computation"},{"key":"15_CR6","series-title":"Lect Notes Comput Sci","first-page":"21","volume-title":"Approximate reachability analysis of piecewise-linear dynamical systems","author":"E. Asarin","year":"2000","unstructured":"E. Asarin, O. Bournez, T. Dang, and O. Maler. Approximate reachability analysis of piecewise-linear dynamical systems. In Hybrid Systems: Computation and Control, Third International Workshop, LNCS 1790, pages 21\u201331. 2000."},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Bebop: A symbolic model checker for boolean programs","author":"T. Ball","year":"2000","unstructured":"T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 2000 Workshop on Model Checking of Software, LNCS 1885. 2000."},{"issue":"6","key":"15_CR8","doi-asserted-by":"publisher","first-page":"915","DOI":"10.1109\/70.650170","volume":"13","author":"S. Cameron","year":"1997","unstructured":"S. Cameron. A comparison of two fast algorithms for computing the distance between convex polyhedra. IEEE Transactions on Robotics and Automation, 13(6):915\u2013920, 1997.","journal-title":"IEEE Transactions on Robotics and Automation"},{"key":"15_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-48983-5_10","volume-title":"Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations","author":"A. Chutinan","year":"1999","unstructured":"A. Chutinan and B.K. Krogh. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In Hybrid Systems: Computation and Control, Second International Workshop, LNCS 1569, pages 76\u201390. 1999."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"E. Clarke, A. Fehnker, Z. Han, B. Krogh, O. Stursberg, and M. Theobald. Verification of hybrid systems based on counterexample-guided abstraction refinement. In Tools and Algorithms for the Construction and Analysis of Systems, 2003.","DOI":"10.1007\/3-540-36577-X_14"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154\u2013169, 2000.","DOI":"10.1007\/10722167_15"},{"issue":"6","key":"15_CR12","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"E.M. Clarke","year":"1996","unstructured":"E.M. Clarke and R.P. Kurshan. Computer-aided Verification. IEEE Spectrum, 33(6):61\u201367, 1996.","journal-title":"IEEE Spectrum"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"J.C. Corbett, M.B. Dwyer, J. Hatcli., S. Laubach, C.S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of 22nd International Conference on Software Engineering. 2000.","DOI":"10.1145\/337180.337234"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a uniffied lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM Symposium on Principles of Programming Languages, 1977.","DOI":"10.1145\/512950.512973"},{"key":"15_CR15","unstructured":"G. Das and D. Joseph. The complexity of minimum convex nested polyhedra. In Canadian Conference on Computational Geometry, 1990."},{"key":"15_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0032342","volume-title":"Hybrid Systems III: Verification and Control","author":"C. Daws","year":"1996","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool kronos. In Hybrid Systems III: Verification and Control, LNCS 1066. Springer-Verlag, 1996."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"D. Dobkin and D. Kirkpatrick. Determining the separation of preprocessed polyhedra \u2014 a unified approach. In Proc. of ICALP\u201990, pages 400\u2013413, 1990.","DOI":"10.1007\/BFb0032047"},{"key":"15_CR18","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1016\/0890-5401(88)90049-1","volume":"77","author":"H. Edelsbrunner","year":"1987","unstructured":"H. Edelsbrunner and F.P. Preparata. Minimum polygon separation. Information and Computation, 77:218\u2013232, 1987.","journal-title":"Information and Computation"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, P. Ho, and H. Wong-Toi. HyTech: the next generation. In Proceedings of the 16th IEEE Real-Time Systems Symposium, pages 56\u201365, 1995.","DOI":"10.1109\/REAL.1995.495196"},{"issue":"5","key":"15_CR20","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"15_CR21","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1002\/bltj.2223","volume":"5","author":"G.J. Holzmann","year":"2000","unstructured":"G.J. Holzmann and M.H. Smith. Automating software feature Verification. Bell Labs Technical Journal, 5(2):72\u201387, 2000.","journal-title":"Bell Labs Technical Journal"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"K. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Springer International Journal of Software Tools for Technology Transfer, 1, 1997.","DOI":"10.1007\/s100090050010"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the Verification of concurrent systems. Formal Methods in System Design Volume 6, Issue 1, 1995.","DOI":"10.1007\/BF01384313"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:47:57Z","timestamp":1558982877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540008989"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}