{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:27:44Z","timestamp":1778498864844,"version":"3.51.4"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,1,21]],"date-time":"2015-01-21T00:00:00Z","timestamp":1421798400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["11371143, 11471209, 91118007, and 61321064"],"award-info":[{"award-number":["11371143, 11471209, 91118007, and 61321064"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Innovation Program of Shanghai Municipal Education Commission","award":["14ZZ046"],"award-info":[{"award-number":["14ZZ046"]}]},{"DOI":"10.13039\/501100004731","name":"Natural Science Foundation of Zhejiang Province","doi-asserted-by":"crossref","award":["LQ13F020041 and LY13F030005"],"award-info":[{"award-number":["LQ13F020041 and LY13F030005"]}],"id":[{"id":"10.13039\/501100004731","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,1,21]]},"abstract":"<jats:p>In this article, we address the problem of safety verification of nonlinear hybrid systems. A hybrid symbolic-numeric method is presented to compute exact inequality invariants of hybrid systems efficiently. Some numerical invariants of a hybrid system can be obtained by solving a bilinear SOS programming via the PENBMI solver or iterative method, then the modified Newton refinement and rational vector recovery techniques are applied to obtain exact polynomial invariants with rational coefficients, which exactly satisfy the conditions of invariants. Experiments on some benchmarks are given to illustrate the efficiency of our algorithm.<\/jats:p>","DOI":"10.1145\/2629424","type":"journal-article","created":{"date-parts":[[2015,1,28]],"date-time":"2015-01-28T14:05:51Z","timestamp":1422453951000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation"],"prefix":"10.1145","volume":"14","author":[{"given":"Zhengfeng","family":"Yang","sequence":"first","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wang","family":"Lin","sequence":"additional","affiliation":[{"name":"Wenzhou University and East China Normal University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Wu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,1,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132357.1132363"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2175058"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2010.2046926"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2002.806655"},{"key":"e_1_2_1_5_1","unstructured":"Mohab Safey El Din. 2003. RAGLib (Real Algebraic Library Maple Package). Available at http:\/\/www- calfor.lip6.fr\/&sim;safey\/RAGLib.  Mohab Safey El Din. 2003. RAGLib (Real Algebraic Library Maple Package). Available at http:\/\/www- calfor.lip6.fr\/&sim;safey\/RAGLib."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/261320.261324"},{"key":"e_1_2_1_7_1","unstructured":"G. H. Golub and C. F. Van Loan. 1996. Matrix Computations (3rd ed.). Johns Hopkins University Press.   G. H. Golub and C. F. Van Loan. 1996. Matrix Computations (3rd ed.). Johns Hopkins University Press."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788803"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390768.1390792"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2011.08.002"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1080\/1055678031000098773"},{"key":"e_1_2_1_13_1","unstructured":"M. Ko\u010dvara and M. Stingl. 2005. PENBMI User\u2019s Guide (Version 2.0). (2005). Available at http:\/\/www.penopt.com.  M. Ko\u010dvara and M. Stingl. 2005. PENBMI User\u2019s Guide (Version 2.0). (2005). Available at http:\/\/www.penopt.com."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0472"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1137\/0214016"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"J. B. Lasserre. 2010. Moments Positive Polynomials and Their Applications. Imperial College Press.  J. B. Lasserre. 2010. Moments Positive Polynomials and Their Applications. Imperial College Press.","DOI":"10.1142\/p665"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/S1052623400375865"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-014-5083-y"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038659"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-003-0387-5"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"A. Platzer and E. M. Clarke. 2007. The image computation problem in hybrid systems model checking. In Hybrid Systems: Computation and Control HSCC. Springer 473--486.   A. Platzer and E. M. Clarke. 2007. The image computation problem in hybrid systems model checking. In Hybrid Systems: Computation and Control HSCC. Springer 473--486.","DOI":"10.1007\/978-3-540-71493-4_37"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0079-8"},{"key":"e_1_2_1_23_1","unstructured":"S. Prajna. 2005. Optimization-Based Methods for Nonlinear and Hybrid Systems Verification. Ph.D. Dissertation. California Institute of Technology.   S. Prajna. 2005. Optimization-Based Methods for Nonlinear and Hybrid Systems Verification. Ph.D. Dissertation. California Institute of Technology."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 7th International Workshop on Hybrid Systems: Computation and Control. 477--492","author":"Prajna S."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11856290_18"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1210268.1210276"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/090749955"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_38"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0046-1"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 17th IFAC World Congress. 6932--6937","author":"Shah G. A."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185632.2185639"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993886.1993935"},{"key":"e_1_2_1_33_1","first-page":"514","article-title":"Approximate reachability for linear systems. In Hybrid Systems: Computation and Control","volume":"2623","author":"Tiwari A.","year":"2003","journal-title":"HSCC (LNCS)"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2331684.2331701"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1358190.1358197"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2006.10.009"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"M. H. Zaki S. Tahar and G. Bois. 2007a. Combining Constraint Solving and Formal Methods for the Verification of Analog Designs. Technical Report. Concordia University.  M. H. Zaki S. Tahar and G. Bois. 2007a. Combining Constraint Solving and Formal Methods for the Verification of Analog Designs. Technical Report. Concordia University.","DOI":"10.1109\/FAMCAD.2007.25"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the International Conference on Computational Sciences. 93--100","author":"Zaki M. H."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629424","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629424","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:30Z","timestamp":1750231170000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629424"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,21]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1,21]]}},"alternative-id":["10.1145\/2629424"],"URL":"https:\/\/doi.org\/10.1145\/2629424","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,21]]},"assertion":[{"value":"2013-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}