{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:12:41Z","timestamp":1761487961517},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540009139"},{"type":"electronic","value":"9783540365808"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36580-x_4","type":"book-chapter","created":{"date-parts":[[2007,12,9]],"date-time":"2007-12-09T12:13:36Z","timestamp":1197202416000},"page":"4-19","source":"Crossref","is-referenced-by-count":38,"title":["Progress on Reachability Analysis of Hybrid Systems Using Predicate Abstraction"],"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","published-online":{"date-parts":[[2003,3,14]]},"reference":[{"key":"4_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":"4_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":"4_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, T. Dang, and F. Ivan\u010di\u0107. Reachability analysis of hybrid systems using counter-example guided predicate abstraction. Technical Report MS-CIS-02-34, University of Pennsylvania, November 2002.","DOI":"10.1007\/3-540-45873-5_6"},{"key":"4_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45873-5_6","volume-title":"Hybrid Systems: Computation and Control, Fifth International Workshop","author":"R. Alur","year":"2002","unstructured":"R. Alur, T. Dang, and F. Ivan\u010di\u0107. Reachability analysis of hybrid systems via predicate abstraction. In Hybrid Systems: Computation and Control, Fifth International Workshop, LNCS 2289, pages 35\u201348, March 2002."},{"key":"4_CR5","unstructured":"R. Alur, T. Dang, and F. Ivan\u010di\u0107. Counter-example guided predicate abstraction of hybrid systems. In Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, April 2003."},{"key":"4_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46430-1_6","volume-title":"Hybrid Systems: Computation and Control, Third International Workshop","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. Springer, 2000."},{"key":"4_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45420-9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"T. Ball, A. Podelski, and S. Rajamani. Boolean and Cartesian abstraction for model checking C programs. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2031. Springer, 2001."},{"key":"4_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_7","volume-title":"SPIN 2000 Workshop on Model Checking of Software","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."},{"key":"4_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48983-5_10","volume-title":"Hybrid Systems: Computation and Control, Second International Workshop","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. Springer, 1999."},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E. M. Clarke","year":"2001","unstructured":"E. M. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in Systems Design, 19(1):7\u201334, 2001.","journal-title":"Formal Methods in Systems Design"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of the 4th ACM Symposium on Principles of Programming Languages, 1977.","DOI":"10.1145\/512950.512973"},{"key":"4_CR12","unstructured":"T. Dang. Verification and Synthesis of Hybrid Systems. PhD thesis, Institut National Polytecnique de Grenoble, 2000."},{"key":"4_CR13","unstructured":"A. R. Girard. Hybrid System Architectures for Coordinated Vehicle Control. PhD thesis, University of California at Berkeley, 2002."},{"key":"4_CR14","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"},{"key":"4_CR15","unstructured":"F. Ivan\u010di\u0107. Report on verification of the MoBIES vehicle-vehicle automotive OEP problem. Technical Report MS-CIS-02-02, University of Pennsylvania, March 2002."},{"key":"4_CR16","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"},{"key":"4_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46430-1_27","volume-title":"Hybrid Systems: Computation and Control","author":"I. Mitchell","year":"2000","unstructured":"I. Mitchell and C. Tomlin. Level set methods for computation in hybrid systems. In Hybrid Systems: Computation and Control, LNCS 1790. Springer, 2000."},{"key":"4_CR18","unstructured":"O. Stursberg, S. Kowalewski, and S. Engell. Generating timed discrete models of continuous systems. In Proc. 2nd IMACS Symposium on Mathematical Modeling, pages 203\u2013209, 1997."},{"key":"4_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control, Fifth Intern. Workshop","author":"A. Tiwari","year":"2002","unstructured":"A. Tiwari and G. Khanna. Series of abstractions for hybrid automata. In Hybrid Systems: Computation and Control, Fifth Intern. Workshop, LNCS 2289, 2002."}],"container-title":["Lecture Notes in Computer Science","Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36580-X_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T06:40:31Z","timestamp":1684132831000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36580-X_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540009139","9783540365808"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-36580-x_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}