{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:48:59Z","timestamp":1725792539289},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319061993"},{"type":"electronic","value":"9783319062006"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06200-6_14","type":"book-chapter","created":{"date-parts":[[2014,4,23]],"date-time":"2014-04-23T05:53:48Z","timestamp":1398232428000},"page":"188-202","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Hybrid Systems Involving Transcendental Functions"],"prefix":"10.1007","author":[{"given":"Paul","family":"Jackson","sequence":"first","affiliation":[]},{"given":"Andrew","family":"Sogokon","sequence":"additional","affiliation":[]},{"given":"James","family":"Bridge","sequence":"additional","affiliation":[]},{"given":"Lawrence","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Ahmadi, A.A., Krstic, M., Parrilo, P.A.: A globally asymptotically stable polynomial vector field with no polynomial Lyapunov function. In: CDC-ECE, pp. 7579\u20137580 (2011)","DOI":"10.1109\/CDC.2011.6161499"},{"issue":"4","key":"14_CR2","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"C.W. Brown","year":"2003","unstructured":"Brown, C.W.: Qepcad b: a program for computing with semi-algebraic sets using cads. SIGSAM Bull.\u00a037(4), 97\u2013108 (2003), \n                  \n                    http:\/\/doi.acm.org\/10.1145\/968708.968710","journal-title":"SIGSAM Bull."},{"issue":"6","key":"14_CR3","doi-asserted-by":"publisher","first-page":"1536","DOI":"10.1016\/j.automatica.2009.02.011","volume":"45","author":"G. Chesi","year":"2009","unstructured":"Chesi, G.: Estimating the domain of attraction for non-polynomial systems via LMI optimizations. Automatica\u00a045(6), 1536\u20131541 (2009)","journal-title":"Automatica"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Denman, W., Akbarpour, B., Tahar, S., Zaki, M., Paulson, L.: Formal verification of analog designs using metitarski. In: Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 93\u2013100 (2009)","DOI":"10.1109\/FMCAD.2009.5351136"},{"issue":"3","key":"14_CR5","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: Hysat: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design\u00a030(3), 179\u2013198 (2007)","journal-title":"Formal Methods in System Design"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: Spaceex: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1017\/CBO9780511807930.002","volume-title":"Handbook of Hybrid Systems Control \u2013 Theory, Tools, Applications, ch. 1","author":"W. Heemels","year":"2009","unstructured":"Heemels, W., Lehmann, D., Lunze, J., De Schutter, B.: Introduction to hybrid systems. In: Lunze, J., Lamnabhi-Lagarrigue, F. (eds.) Handbook of Hybrid Systems Control \u2013 Theory, Tools, Applications, ch. 1, pp. 3\u201330. Cambridge University Press, Cambridge (2009)"},{"issue":"1-2","key":"14_CR8","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: A model checker for hybrid systems. STTT\u00a01(1-2), 110\u2013122 (1997)","journal-title":"STTT"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-32347-8_1","volume-title":"Interactive Theorem Proving","author":"L.C. Paulson","year":"2012","unstructured":"Paulson, L.C.: MetiTarski: Past and Future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 1\u201310. Springer, Heidelberg (2012)"},{"key":"14_CR11","unstructured":"Paulson, L.C.: University of Cambridge (2013), \n                  \n                    http:\/\/www.cl.cam.ac.uk\/~lp15\/papers\/Arith\/"},{"key":"14_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A. Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)"},{"key":"14_CR13","unstructured":"Platzer, A.: Carnegie Mellon Uniersity (2013), \n                  \n                    http:\/\/symbolaris.com\/info\/KeYmaera.html"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S. Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 477\u2013492. Springer, Heidelberg (2004)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embedded Comput. Syst.\u00a06(1) (2007)","DOI":"10.1145\/1210268.1210276"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06200-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T17:17:11Z","timestamp":1558891031000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06200-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319061993","9783319062006"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06200-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}