{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T23:10:00Z","timestamp":1768345800937,"version":"3.49.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2006,2,1]],"date-time":"2006-02-01T00:00:00Z","timestamp":1138752000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2006,2]]},"abstract":"<jats:p>\n            Embedded systems are increasingly finding their way into a growing range of physical devices. These embedded systems often consist of a collection of software threads interacting concurrently with each other and with a physical, continuous environment. While continuous dynamics have been well studied in control theory, and discrete and distributed systems have been investigated in computer science, the combination of the two complexities leads us to the recent research on\n            <jats:italic>hybrid systems<\/jats:italic>\n            . This paper addresses the formal analysis of such hybrid systems. Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state discrete programs. This paper presents algorithms and tools for reachability analysis of hybrid systems by combining the notion of predicate abstraction with recent techniques for approximating the set of reachable states of linear systems using polyhedra. Given a hybrid system and a set of predicates, we consider the finite discrete quotient whose states correspond to all possible truth assignments to the input predicates. The tool performs an on-the-fly exploration of the abstract system. We present the basic techniques for guided search in the abstract state-space, optimizations of these techniques, implementation of these in our verifier, and case studies demonstrating the promise of the approach. We also address the completeness of our abstraction-based verification strategy by showing that predicate abstraction of hybrid systems can be used to prove bounded safety.\n          <\/jats:p>","DOI":"10.1145\/1132357.1132363","type":"journal-article","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:14:26Z","timestamp":1153836866000},"page":"152-199","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":81,"title":["Predicate abstraction for reachability analysis of hybrid systems"],"prefix":"10.1145","volume":"5","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}]},{"given":"Thao","family":"Dang","sequence":"additional","affiliation":[{"name":"Verimag, Gieres, France"}]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[{"name":"NEC Laboratories America, Princeton, NJ"}]}],"member":"320","published-online":{"date-parts":[[2006,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1059"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"e_1_2_1_5_1","volume-title":"Third International Workshop.","volume":"1790","author":"Alur R.","unstructured":"Alur , R. , Grosu , R. , Hur , Y. , Kumar , V. , and Lee , I . 2000a. Modular specifications of hybrid systems in charon. In Hybrid Systems: Computation and Control , Third International Workshop. Vol. LNCS 1790 . 6--19.]] Alur, R., Grosu, R., Hur, Y., Kumar, V., and Lee, I. 2000a. Modular specifications of hybrid systems in charon. In Hybrid Systems: Computation and Control, Third International Workshop. Vol. LNCS 1790. 6--19.]]"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the IEEE.]]","author":"Alur R.","unstructured":"Alur , R. , Henzinger , T. , Lafferriere , G. , and Pappas , G . 2000b. Discrete abstractions of hybrid systems . Proceedings of the IEEE.]] Alur, R., Henzinger, T., Lafferriere, G., and Pappas, G. 2000b. Discrete abstractions of hybrid systems. Proceedings of the IEEE.]]"},{"key":"e_1_2_1_7_1","volume-title":"Fifth International Workshop, C. Tomlin and M. Greenstreet, Eds. LNCS 2289","author":"Alur R.","unstructured":"Alur , R. , Dang , T. , and Ivan\u010di\u0107 , F . 2002. Reachability analysis of hybrid systems via predicate abstraction. In Hybrid Systems: Computation and Control , Fifth International Workshop, C. Tomlin and M. Greenstreet, Eds. LNCS 2289 . Springer-Verlag, New York, 35--48.]] Alur, R., Dang, T., and Ivan\u010di\u0107, F. 2002. Reachability analysis of hybrid systems via predicate abstraction. In Hybrid Systems: Computation and Control, Fifth International Workshop, C. Tomlin and M. Greenstreet, Eds. LNCS 2289. Springer-Verlag, New York, 35--48.]]"},{"key":"e_1_2_1_8_1","volume-title":"Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems.]]","author":"Alur R.","unstructured":"Alur , R. , Dang , T. , and Ivan\u010di\u0107 , F . 2003a. Counter-example guided predicate abstraction of hybrid systems . In Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems.]] Alur, R., Dang, T., and Ivan\u010di\u0107, F. 2003a. Counter-example guided predicate abstraction of hybrid systems. In Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems.]]"},{"key":"e_1_2_1_9_1","volume-title":"Sixth International Workshop.]]","author":"Alur R.","unstructured":"Alur , R. , Dang , T. , and Ivan\u010di\u0107 , F . 2003b. Progress on reachability analysis of hybrid systems via predicate abstraction. In Hybrid Systems: Computation and Control , Sixth International Workshop.]] Alur, R., Dang, T., and Ivan\u010di\u0107, F. 2003b. Progress on reachability analysis of hybrid systems via predicate abstraction. In Hybrid Systems: Computation and Control, Sixth International Workshop.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/JPROC.2002.805817","article-title":"Hierarchical modeling and analysis of embedded systems","volume":"91","author":"Alur R.","year":"2003","unstructured":"Alur , R. , Dang , T. , Esposito , J. , Hur , Y. , Ivan\u010di\u0107 , F. , Kumar , V. , Lee , I. , Mishra , P. , Pappas , G. , and Sokolsky , O. 2003 c. Hierarchical modeling and analysis of embedded systems . Proceedings of the IEEE 91 , 1 (Jan.).]] Alur, R., Dang, T., Esposito, J., Hur, Y., Ivan\u010di\u0107, F., Kumar, V., Lee, I., Mishra, P., Pappas, G., and Sokolsky, O. 2003c. Hierarchical modeling and analysis of embedded systems. Proceedings of the IEEE 91, 1 (Jan.).]]","journal-title":"Proceedings of the IEEE"},{"key":"e_1_2_1_11_1","volume-title":"Third International Workshop. LNCS 1790","author":"Asarin E.","unstructured":"Asarin , E. , Bournez , O. , Dang , T. , and Maler , O . 2000. Approximate reachability analysis of piecewise-linear dynamical systems. In Hybrid Systems: Computation and Control , Third International Workshop. LNCS 1790 . Springer Verlag, New York. 21--31.]] Asarin, E., Bournez, O., Dang, T., and Maler, O. 2000. Approximate reachability analysis of piecewise-linear dynamical systems. In Hybrid Systems: Computation and Control, Third International Workshop. LNCS 1790. Springer Verlag, New York. 21--31.]]"},{"key":"e_1_2_1_12_1","volume-title":"SPIN 2000 Workshop on Model Checking of Software. LNCS","author":"Ball T.","year":"1885","unstructured":"Ball , T. and Rajamani , S . 2000. Bebop: A symbolic model checker for boolean programs . In SPIN 2000 Workshop on Model Checking of Software. LNCS 1885 . Springer, New York. 113--130.]] Ball, T. and Rajamani, S. 2000. Bebop: A symbolic model checker for boolean programs. In SPIN 2000 Workshop on Model Checking of Software. LNCS 1885. Springer, New York. 113--130.]]"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/235815.235821"},{"key":"e_1_2_1_14_1","volume-title":"11th International Conference. LNCS","volume":"1633","author":"Behrmann G.","unstructured":"Behrmann , G. , Larsen , K. , Pearson , J. , Weise , C. , and Yi , W . 1999. Efficient timed reachability analysis using clock difference diagrams. In Computer Aided Verification , 11th International Conference. LNCS , vol. 1633 . Springer-Verlag, New York.]] Behrmann, G., Larsen, K., Pearson, J., Weise, C., and Yi, W. 1999. Efficient timed reachability analysis using clock difference diagrams. In Computer Aided Verification, 11th International Conference. LNCS, vol. 1633. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of International Workshop on Software Tools for Technology Transfer.]]","author":"Bengsston J.","unstructured":"Bengsston , J. , Larsen , K. , Larsson , F. , Pettersson , P. , Yi , W. , and Weise , C . 1998. New generation of uppaal . In Proceedings of International Workshop on Software Tools for Technology Transfer.]] Bengsston, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W., and Weise, C. 1998. New generation of uppaal. In Proceedings of International Workshop on Software Tools for Technology Transfer.]]"},{"key":"e_1_2_1_16_1","volume-title":"LFM 2000: Fifth NASA Langley Formal Methods Workshop, C. M. Holloway, Ed","author":"Bensalem S.","unstructured":"Bensalem , S. , Ganesh , V. , Lakhnech , Y. , noz, C. M., Owre , S. , Ruess , H. , Rushby , J. , Rusu , V. , Sa\u00efdi , H. , Shankar , N. , Singerman , E. , and Tiwari , A . 2000. An overview of SAL . In LFM 2000: Fifth NASA Langley Formal Methods Workshop, C. M. Holloway, Ed . Hampton, VA. 187--196.]] Bensalem, S., Ganesh, V., Lakhnech, Y., noz, C. M., Owre, S., Ruess, H., Rushby, J., Rusu, V., Sa\u00efdi, H., Shankar, N., Singerman, E., and Tiwari, A. 2000. An overview of SAL. In LFM 2000: Fifth NASA Langley Formal Methods Workshop, C. M. Holloway, Ed. Hampton, VA. 187--196.]]"},{"key":"e_1_2_1_17_1","volume-title":"Second International Workshop. LNCS 1569","author":"Chutinan A.","unstructured":"Chutinan , A. and Krogh , B . 1999. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In Hybrid Systems: Computation and Control , Second International Workshop. LNCS 1569 . Springer-Verlag, New York. 76--90.]] Chutinan, A. and Krogh, B. 1999. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In Hybrid Systems: Computation and Control, Second International Workshop. LNCS 1569. Springer-Verlag, New York. 76--90.]]"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 2000 American Control Conference.]]","author":"Chutinan A.","unstructured":"Chutinan , A. and Krogh , B . 2000. Approximate quotient transition systems for hybrid systems . In Proceedings of the 2000 American Control Conference.]] Chutinan, A. and Krogh, B. 2000. Approximate quotient transition systems for hybrid systems. In Proceedings of the 2000 American Control Conference.]]"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Clarke E. Grumberg O. and Long D. 1993. Verification tools for finite-state concurrent systems. In Decade of Concurrency---Reflections and Perspectives (Proceedings of REX School). LNCS 803. Springer-Verlag New York. 124--175.]]   Clarke E. Grumberg O. and Long D. 1993. Verification tools for finite-state concurrent systems. In Decade of Concurrency---Reflections and Perspectives (Proceedings of REX School). LNCS 803. Springer-Verlag New York. 124--175.]]","DOI":"10.1007\/3-540-58043-3_19"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Clarke E. Grumberg O. Jha S. Lu Y. and Veith H. 2000. Counterexample-guided abstraction refinement. In Computer Aided Verification. 154--169.]]   Clarke E. Grumberg O. Jha S. Lu Y. and Veith H. 2000. Counterexample-guided abstraction refinement. In Computer Aided Verification. 154--169.]]","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1142\/S012905410300190X","article-title":"Abstraction and counterexample-guided refinement of hybrid systems","volume":"14","author":"Clarke E.","year":"2003","unstructured":"Clarke , E. , Fehnker , A. , Han , Z. , Krogh , B. , Ouaknine , J. , Stursberg , O. , and Theobald , M. 2003 a. Abstraction and counterexample-guided refinement of hybrid systems . Intern. Journal of Foundations of Computer Science 14 , 4 (Aug.), 583--604.]] Clarke, E., Fehnker, A., Han, Z., Krogh, B., Ouaknine, J., Stursberg, O., and Theobald, M. 2003a. Abstraction and counterexample-guided refinement of hybrid systems. Intern. Journal of Foundations of Computer Science 14, 4 (Aug.), 583--604.]]","journal-title":"Intern. Journal of Foundations of Computer Science"},{"key":"e_1_2_1_23_1","volume-title":"Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems.]]","author":"Clarke E.","unstructured":"Clarke , E. , Fehnker , A. , Han , Z. , Krogh , B. , Stursberg , O. , and Theobald , M . 2003b. Verification of hybrid systems based on counterexample-guided abstraction refinement . In Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems.]] Clarke, E., Fehnker, A., Han, Z., Krogh, B., Stursberg, O., and Theobald, M. 2003b. Verification of hybrid systems based on counterexample-guided abstraction refinement. In Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems.]]"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/6.499951"},{"key":"e_1_2_1_25_1","volume-title":"Embedded, Everywhere: A Research Agenda for Networked Systems of Embedded Computers.]]","author":"Computer Science","year":"2001","unstructured":"Computer Science and Telecommunications Board. 2001 . Embedded, Everywhere: A Research Agenda for Networked Systems of Embedded Computers.]] Computer Science and Telecommunications Board. 2001. Embedded, Everywhere: A Research Agenda for Networked Systems of Embedded Computers.]]"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of 22nd International Conference on Software Engineering. 439--448","author":"Corbett J.","unstructured":"Corbett , J. , Dwyer , M. , Hatcliff , J. , Laubach , S. , Pasareanu , C. , Robby , and Zheng, H . 2000. Bandera: Extracting finite-state models from Java source code . In Proceedings of 22nd International Conference on Software Engineering. 439--448 .]] 10.1145\/337180.337234 Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, and Zheng, H. 2000. Bandera: Extracting finite-state models from Java source code. In Proceedings of 22nd International Conference on Software Engineering. 439--448.]] 10.1145\/337180.337234"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 4th ACM Symposium on Principles of Programming Languages. 238--252","author":"Cousot P.","unstructured":"Cousot , P. and Cousot , R . 1977. Abstract interpretation: a unified 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. 238--252 .]] 10.1145\/512950.512973 Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified 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. 238--252.]] 10.1145\/512950.512973"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/9.664159","article-title":"Synthesis of supervisory controller for hybrid systems based on approximating automata","volume":"43","author":"Cury J.","year":"1998","unstructured":"Cury , J. , Krogh , B. , and Niinomi , T. 1998 . Synthesis of supervisory controller for hybrid systems based on approximating automata . IEEE Transaction on Automatic Control 43 , 4 (Apr.), 564--569.]] Cury, J., Krogh, B., and Niinomi, T. 1998. Synthesis of supervisory controller for hybrid systems based on approximating automata. IEEE Transaction on Automatic Control 43, 4 (Apr.), 564--569.]]","journal-title":"IEEE Transaction on Automatic Control"},{"key":"e_1_2_1_30_1","volume-title":"Hybrid Systems: Computation and Control. LNCS","volume":"1386","author":"Dang T.","unstructured":"Dang , T. and Maler , O . 1998. Reachability analysis via face-lifting . In Hybrid Systems: Computation and Control. LNCS , vol. 1386 . Springer-Verlag, New York. 96--109.]] Dang, T. and Maler, O. 1998. Reachability analysis via face-lifting. In Hybrid Systems: Computation and Control. LNCS, vol. 1386. Springer-Verlag, New York. 96--109.]]"},{"key":"e_1_2_1_31_1","volume-title":"11th International Conference. LNCS 1633","author":"Das S.","unstructured":"Das , S. , Dill , D. , and Park , S . 1999. Experience with predicate abstraction. In Computer Aided Verification , 11th International Conference. LNCS 1633 . Springer, New York. 160--171.]] Das, S., Dill, D., and Park, S. 1999. Experience with predicate abstraction. In Computer Aided Verification, 11th International Conference. LNCS 1633. Springer, New York. 160--171.]]"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Daws C. Olivero A. Tripakis S. and Yovine S. 1996. The tool kronos. In Hybrid Systems III: Verification and Control. LNCS 1066. Springer-Verlag New York. 208--219.]]   Daws C. Olivero A. Tripakis S. and Yovine S. 1996. The tool kronos. In Hybrid Systems III: Verification and Control. LNCS 1066. Springer-Verlag New York. 208--219.]]","DOI":"10.1007\/BFb0020947"},{"key":"e_1_2_1_33_1","volume-title":"CAV","volume":"3114","author":"de Moura L.","year":"2004","unstructured":"de Moura , L. , Owre , S. , Rue\u00df , H. , Rushby , J. , Shankar , N. , Sorea , M. , and Tiwari , A . 2004. SAL 2. In Computer-Aided Verification , CAV 2004 , R. Alur and D. Peled, Eds. Lecture Notes in Computer Science , vol. 3114 . Springer-Verlag, New York, 496--500.]] de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., and Tiwari, A. 2004. SAL 2. In Computer-Aided Verification, CAV 2004, R. Alur and D. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, New York, 496--500.]]"},{"key":"e_1_2_1_34_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"2993","author":"Fehnker A.","unstructured":"Fehnker , A. and Ivan\u010di\u0107 , F . 2004. Benchmarks for hybrid systems verification. In Hybrid Systems: Computation and Control, R. Alur and G. Pappas , Eds. Lecture Notes in Computer Science , vol. 2993 . Springer, New York. 326--341.]] Fehnker, A. and Ivan\u010di\u0107, F. 2004. Benchmarks for hybrid systems verification. In Hybrid Systems: Computation and Control, R. Alur and G. Pappas, Eds. Lecture Notes in Computer Science, vol. 2993. Springer, New York. 326--341.]]"},{"key":"e_1_2_1_35_1","unstructured":"Fehnker A. Clarke E. Jha S. and Krogh B. 2005. Refining abstractions of hybrid systems using counterexample fragments. In Hybrid Systems:Computation and Control (HSCC). LNCS. Springer.]] 10.1007\/978-3-540-31954-2_16   Fehnker A. Clarke E. Jha S. and Krogh B. 2005. Refining abstractions of hybrid systems using counterexample fragments. In Hybrid Systems:Computation and Control (HSCC). LNCS. Springer.]] 10.1007\/978-3-540-31954-2_16"},{"key":"e_1_2_1_36_1","volume-title":"cddlib reference manual, cddlib version 092a. Tech. rep","author":"Fukuda K.","unstructured":"Fukuda , K. 2001. cddlib reference manual, cddlib version 092a. Tech. rep ., McGill University .]] Fukuda, K. 2001. cddlib reference manual, cddlib version 092a. Tech. rep., McGill University.]]"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","first-page":"1125","DOI":"10.1109\/25.330177","article-title":"Longitudinal control of a lead card of a platoon","volume":"43","author":"Godbole D.","year":"1994","unstructured":"Godbole , D. and Lygeros , J. 1994 . Longitudinal control of a lead card of a platoon . IEEE Transactions on Vehicular Technology 43 , 4, 1125 -- 1135 .]] Godbole, D. and Lygeros, J. 1994. Longitudinal control of a lead card of a platoon. IEEE Transactions on Vehicular Technology 43, 4, 1125--1135.]]","journal-title":"IEEE Transactions on Vehicular Technology"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","article-title":"Abstraction-based model checking using modal transition systems. In 12th International Conference on Concurrency Theory","volume":"2154","author":"Godefroid P.","year":"2001","unstructured":"Godefroid , P. , Huth , M. , and Jagadeesan , R. 2001 . Abstraction-based model checking using modal transition systems. In 12th International Conference on Concurrency Theory . Lecture Notes in Computer Science , vol. 2154. 426 -- 440 .]] Godefroid, P., Huth, M., and Jagadeesan, R. 2001. Abstraction-based model checking using modal transition systems. In 12th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 2154. 426--440.]]","journal-title":"Lecture Notes in Computer Science"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97)","volume":"1254","author":"Graf S.","unstructured":"Graf , S. and Saidi , H . 1997. Construction of abstract state graphs with PVS . In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97) , vol. 1254 . Springer Verlag, New York. 72--83.]] Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), vol. 1254. Springer Verlag, New York. 72--83.]]"},{"key":"e_1_2_1_41_1","volume-title":"Second International Workshop. LNCS 1569","author":"Greenstreet M.","unstructured":"Greenstreet , M. and Mitchell , I . 1999. Reachability analysis using polygonal projections. In Hybrid Systems: Computation and Control , Second International Workshop. LNCS 1569 . Springer-Verlag, New York. 103--116.]] Greenstreet, M. and Mitchell, I. 1999. Reachability analysis using polygonal projections. In Hybrid Systems: Computation and Control, Second International Workshop. LNCS 1569. Springer-Verlag, New York. 103--116.]]"},{"key":"e_1_2_1_42_1","volume-title":"International Symposium on Static Analysis. LNCS 864","author":"Halbwachs N.","unstructured":"Halbwachs , N. , Proy , Y. , and Raymond , P . 1994. Verification of linear hybrid systems by means of convex approximations . In International Symposium on Static Analysis. LNCS 864 . Springer-Verlag, New York.]] Halbwachs, N., Proy, Y., and Raymond, P. 1994. Verification of linear hybrid systems by means of convex approximations. In International Symposium on Static Analysis. LNCS 864. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 16th IEEE Real-Time Systems Symposium. 56--65","author":"Henzinger T.","unstructured":"Henzinger , T. , Ho , P. , and Wong-Toi , H . 1995. HyTech: the next generation . In Proceedings of the 16th IEEE Real-Time Systems Symposium. 56--65 .]] Henzinger, T., Ho, P., and Wong-Toi, H. 1995. HyTech: the next generation. In Proceedings of the 16th IEEE Real-Time Systems Symposium. 56--65.]]"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Henzinger T. Ho P. and Wong-Toi H. 1997. HyTech: a model checker for hybrid systems. Software Tools for Technology Transfer 1.]]  Henzinger T. Ho P. and Wong-Toi H. 1997. HyTech: a model checker for hybrid systems. Software Tools for Technology Transfer 1.]]","DOI":"10.1007\/s100090050008"},{"key":"e_1_2_1_45_1","volume-title":"Symposium on Principles of Programming Languages. 58--70","author":"Henzinger T.","unstructured":"Henzinger , T. , Jhala , R. , Majumdar , R. , and Sutre , G . 2002. Lazy abstraction . In Symposium on Principles of Programming Languages. 58--70 .]] 10.1145\/503272.503279 Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Symposium on Principles of Programming Languages. 58--70.]] 10.1145\/503272.503279"},{"key":"e_1_2_1_46_1","volume-title":"Symposium on Principles of Programming Languages. ACM Press","author":"Henzinger T.","year":"2004","unstructured":"Henzinger , T. , Jhala , R. , Majumdar , R. , and McMillan , K. 2004 . Abstractions from proofs . In Symposium on Principles of Programming Languages. ACM Press , New York. 232--244.]] 10.1145\/964001.964021 Henzinger, T., Jhala, R., Majumdar, R., and McMillan, K. 2004. Abstractions from proofs. In Symposium on Principles of Programming Languages. ACM Press, New York. 232--244.]] 10.1145\/964001.964021"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1002\/bltj.2223","article-title":"Automating software feature verification","volume":"5","author":"Holzmann G.","year":"2000","unstructured":"Holzmann , G. and Smith , M. 2000 . Automating software feature verification . Bell Labs Technical J. 5 , 2, 72 -- 87 .]] Holzmann, G. and Smith, M. 2000. Automating software feature verification. Bell Labs Technical J. 5, 2, 72--87.]]","journal-title":"Bell Labs Technical J."},{"key":"e_1_2_1_50_1","volume-title":"11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS","volume":"3340","author":"Jain H.","year":"1980","unstructured":"Jain , H. , Ivan\u010di\u0107 , F. , Gupta , A. , and Ganai , M . 2005. Localization and register sharing for predicate abstraction . In 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS , vol. 3340 . Springer, New York, 397--412.]] 10.1007\/978-3-540-3 1980 -1_26 Jain, H., Ivan\u010di\u0107, F., Gupta, A., and Ganai, M. 2005. Localization and register sharing for predicate abstraction. In 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 3340. Springer, New York, 397--412.]] 10.1007\/978-3-540-31980-1_26"},{"key":"e_1_2_1_51_1","volume-title":"Third International Workshop. LNCS 1790","author":"Kurzhanski A.","unstructured":"Kurzhanski , A. and Varaiya , P . 2000. Ellipsoidal techniques for reachability analysis. In Hybrid Systems: Computation and Control , Third International Workshop. LNCS 1790 . Springer-Verlag, New York. 202--214.]] Kurzhanski, A. and Varaiya, P. 2000. Ellipsoidal techniques for reachability analysis. In Hybrid Systems: Computation and Control, Third International Workshop. LNCS 1790. Springer-Verlag, New York. 202--214.]]"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384313"},{"key":"e_1_2_1_53_1","volume-title":"Third International Workshop. LNCS 1790","author":"Mitchell I.","unstructured":"Mitchell , I. and Tomlin , C . 2000. Level set methods for computation in hybrid systems. In Hybrid Systems: Computation and Control , Third International Workshop. LNCS 1790 . Springer-Verlag, New York. 310--323.]] Mitchell, I. and Tomlin, C. 2000. Level set methods for computation in hybrid systems. In Hybrid Systems: Computation and Control, Third International Workshop. LNCS 1790. Springer-Verlag, New York. 310--323.]]"},{"key":"e_1_2_1_54_1","first-page":"6","article-title":"Predicate abstraction for dense real-time systems","volume":"65","author":"M\u00f6ller M. O.","year":"2002","unstructured":"M\u00f6ller , M. O. , Rue\u00df , H. , and Sorea , M. 2002 . Predicate abstraction for dense real-time systems . Electronic Notes in Theoretical Computer Science 65 , 6 .]] M\u00f6ller, M. O., Rue\u00df, H., and Sorea, M. 2002. Predicate abstraction for dense real-time systems. Electronic Notes in Theoretical Computer Science 65, 6.]]","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_2_1_55_1","volume-title":"Tech. Rep. UBC-ITS-PRR-95-24, California PATH","author":"Puri A.","year":"1995","unstructured":"Puri , A. and Varaiya , P . 1995 . Driving safely in smart cars. Tech. Rep. UBC-ITS-PRR-95-24, California PATH , University of California in Berkeley , Berkeley, CA .]] Puri, A. and Varaiya, P. 1995. Driving safely in smart cars. Tech. Rep. UBC-ITS-PRR-95-24, California PATH, University of California in Berkeley, Berkeley, CA.]]"},{"key":"e_1_2_1_56_1","volume-title":"40th Conference on Decision and Control.]]","author":"Silva B.","unstructured":"Silva , B. , Stursberg , O. , Krogh , B. , and Engell , S . 2001. An assessment of the current status of algorithmic approaches to the verification of hybrid systems . In 40th Conference on Decision and Control.]] Silva, B., Stursberg, O., Krogh, B., and Engell, S. 2001. An assessment of the current status of algorithmic approaches to the verification of hybrid systems. In 40th Conference on Decision and Control.]]"},{"key":"e_1_2_1_57_1","first-page":"5","article-title":"Bounded model checking for timed automata","volume":"68","author":"Sorea M.","year":"2002","unstructured":"Sorea , M. 2002 . Bounded model checking for timed automata . Electronic Notes in Theoretical Computer Science 68 , 5 .]] Sorea, M. 2002. Bounded model checking for timed automata. Electronic Notes in Theoretical Computer Science 68, 5.]]","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_2_1_58_1","volume-title":"Fifth International Workshop, C. Tomlin and M. Greenstreet, Eds. LNCS 2289","author":"Tiwari A.","unstructured":"Tiwari , A. and Khanna , G . 2002. Series of abstractions for hybrid automata. In Hybrid Systems: Computation and Control , Fifth International Workshop, C. Tomlin and M. Greenstreet, Eds. LNCS 2289 . Springer-Verlag, New York. 465--478.]] Tiwari, A. and Khanna, G. 2002. Series of abstractions for hybrid automata. In Hybrid Systems: Computation and Control, Fifth International Workshop, C. Tomlin and M. Greenstreet, Eds. LNCS 2289. Springer-Verlag, New York. 465--478.]]"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1132357.1132363","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1132357.1132363","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:18:50Z","timestamp":1750263530000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1132357.1132363"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,2]]},"references-count":55,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,2]]}},"alternative-id":["10.1145\/1132357.1132363"],"URL":"https:\/\/doi.org\/10.1145\/1132357.1132363","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2]]},"assertion":[{"value":"2006-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}