{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:54:54Z","timestamp":1740099294837,"version":"3.37.3"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,4,16]],"date-time":"2020-04-16T00:00:00Z","timestamp":1586995200000},"content-version":"vor","delay-in-days":366,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1837244"],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-18-C-0090"],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N000141712012"],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,4,16]]},"DOI":"10.1145\/3302504.3311806","type":"proceedings-article","created":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T13:37:58Z","timestamp":1554730678000},"page":"169-178","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":144,"title":["Verisig"],"prefix":"10.1145","author":[{"given":"Radoslav","family":"Ivanov","sequence":"first","affiliation":[{"name":"University of Pennsylvania"}]},{"given":"James","family":"Weimer","sequence":"additional","affiliation":[{"name":"University of Pennsylvania"}]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[{"name":"University of Pennsylvania"}]},{"given":"George J.","family":"Pappas","sequence":"additional","affiliation":[{"name":"University of Pennsylvania"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[{"name":"University of Pennsylvania"}]}],"member":"320","published-online":{"date-parts":[[2019,4,16]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"US National Highway Traffic Safety Administration. {n. d.}. Investigation PE 16-007. https:\/\/static.nhtsa.gov\/odi\/inv\/2016\/INCLA-PE16007-7876.pdf. US National Highway Traffic Safety Administration. {n. d.}. Investigation PE 16-007. https:\/\/static.nhtsa.gov\/odi\/inv\/2016\/INCLA-PE16007-7876.pdf."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_3_2_1_3_1","unstructured":"US National Transportation Safety Board. {n. d.}. Preliminary Report Highway HWY18MH010. https:\/\/www.ntsb.gov\/investi-gations\/AccidentReports\/Reports\/HWY18MH010-prelim.pdf. US National Transportation Safety Board. {n. d.}. Preliminary Report Highway HWY18MH010. https:\/\/www.ntsb.gov\/investi-gations\/AccidentReports\/Reports\/HWY18MH010-prelim.pdf."},{"volume-title":"International Conference on Computer Aided Verification. Springer, 258--263","author":"Chen X.","key":"e_1_3_2_1_4_1","unstructured":"X. Chen , E. \u00c1brah\u00e1m , and S. Sankaranarayanan . 2013. Flow*: An analyzer for nonlinear hybrid systems . In International Conference on Computer Aided Verification. Springer, 258--263 . X. Chen, E. \u00c1brah\u00e1m, and S. Sankaranarayanan. 2013. Flow*: An analyzer for nonlinear hybrid systems. In International Conference on Computer Aided Verification. Springer, 258--263."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728607"},{"volume-title":"NASA Formal Methods Symposium. Springer, 357--372","author":"Dreossi T.","key":"e_1_3_2_1_6_1","unstructured":"T. Dreossi , A. Donz\u00e9 , and S. A. Seshia . 2017. Compositional falsification of cyber-physical systems with machine learning components . In NASA Formal Methods Symposium. Springer, 357--372 . T. Dreossi, A. Donz\u00e9, and S. A. Seshia. 2017. Compositional falsification of cyber-physical systems with machine learning components. In NASA Formal Methods Symposium. Springer, 357--372."},{"volume-title":"Output Range Analysis for Deep Feedforward Neural Networks. In NASA Formal Methods Symposium. Springer, 121--138","author":"Dutta S.","key":"e_1_3_2_1_7_1","unstructured":"S. Dutta , S. Jha , S. Sankaranarayanan , and A. Tiwari . 2018 . Output Range Analysis for Deep Feedforward Neural Networks. In NASA Formal Methods Symposium. Springer, 121--138 . S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari. 2018. Output Range Analysis for Deep Feedforward Neural Networks. In NASA Formal Methods Symposium. Springer, 121--138."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032335"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"S. Gao S. Kong W. Chen and E. Clarke. 2014. Delta-complete analysis for bounded reachability of hybrid systems. arXiv preprint arXiv:1404.7171 (2014). S. Gao S. Kong W. Chen and E. Clarke. 2014. Delta-complete analysis for bounded reachability of hybrid systems. arXiv preprint arXiv:1404.7171 (2014).","DOI":"10.21236\/ADA613813"},{"key":"e_1_3_2_1_11_1","unstructured":"I. Goodfellow Y. Bengio A. Courville and Y. Bengio. 2016. Deep learning. Vol. 1. MIT press Cambridge. I. Goodfellow Y. Bengio A. Courville and Y. Bengio. 2016. Deep learning. Vol. 1. MIT press Cambridge."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2018.2843682"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"K. Hornik M. Stinchcombe and H. White. 1989. Multilayer feedforward networks are universal approximators. Neural networks 2 5 (1989) 359--366. K. Hornik M. Stinchcombe and H. White. 1989. Multilayer feedforward networks are universal approximators. Neural networks 2 5 (1989) 359--366.","DOI":"10.1016\/0893-6080(89)90020-8"},{"key":"e_1_3_2_1_14_1","volume-title":"Digital Avionics Systems Conference (DASC)","author":"Julian K. D.","year":"2016","unstructured":"K. D. Julian , J. Lopez , J. S. Brush , M. P. Owen , and M. J. Kochenderfer . 2016. Policy compression for aircraft collision avoidance systems . In Digital Avionics Systems Conference (DASC) , 2016 IEEE\/AIAA 35th. IEEE, 1--10. K. D. Julian, J. Lopez, J. S. Brush, M. P. Owen, and M. J. Kochenderfer. 2016. Policy compression for aircraft collision avoidance systems. In Digital Avionics Systems Conference (DASC), 2016 IEEE\/AIAA 35th. IEEE, 1--10."},{"key":"e_1_3_2_1_15_1","volume-title":"Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification","author":"Katz G.","year":"2017","unstructured":"G. Katz , C. Barrett , D. L. Dill , K. Julian , and M. J. Kochenderfer . 2017 . Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification . Springer , 97--117. G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification. Springer, 97--117."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"M. J. Kearns and U. Vazirani. 1994. An introduction to computational learning theory. MIT press. M. J. Kearns and U. Vazirani. 1994. An introduction to computational learning theory. MIT press.","DOI":"10.7551\/mitpress\/3897.001.0001"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_15"},{"volume-title":"International Workshop on Hybrid Systems: Computation and Control. 137--151","author":"Lafferriere G.","key":"e_1_3_2_1_18_1","unstructured":"G. Lafferriere , G. J. Pappas , and S. Yovine . 1999. A new class of decidable hybrid systems . In International Workshop on Hybrid Systems: Computation and Control. 137--151 . G. Lafferriere, G. J. Pappas, and S. Yovine. 1999. A new class of decidable hybrid systems. In International Workshop on Hybrid Systems: Computation and Control. 137--151."},{"key":"e_1_3_2_1_19_1","unstructured":"T. P. Lillicrap J. J. Hunt A. Pritzel N. Heess T. Erez Y. Tassa D. Silver and D. Wierstra. 2015. Continuous control with deep reinforcement learning. arXiv preprint arXiv:1509.02971 (2015). T. P. Lillicrap J. J. Hunt A. Pritzel N. Heess T. Erez Y. Tassa D. Silver and D. Wierstra. 2015. Continuous control with deep reinforcement learning. arXiv preprint arXiv:1509.02971 (2015)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"V. Mnih etal 2015. Human-level control through deep reinforcement learning. Nature 518 7540 (2015) 529. V. Mnih et al. 2015. Human-level control through deep reinforcement learning. Nature 518 7540 (2015) 529.","DOI":"10.1038\/nature14236"},{"key":"e_1_3_2_1_21_1","unstructured":"M. Mohri A. Rostamizadeh and A. Talwalkar. 2012. Foundations of machine learning. MIT press. M. Mohri A. Rostamizadeh and A. Talwalkar. 2012. Foundations of machine learning. MIT press."},{"volume-title":"International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337--340","author":"Moura L. D.","key":"e_1_3_2_1_22_1","unstructured":"L. D. Moura and N. Bj\u00f8rner . 2008. Z3: An efficient SMT solver . In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337--340 . L. D. Moura and N. Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337--340."},{"key":"e_1_3_2_1_23_1","unstructured":"OpenAI. {n. d.}. OpenAI Gym. https:\/\/gym.openai.com. OpenAI. {n. d.}. OpenAI Gym. https:\/\/gym.openai.com."},{"key":"e_1_3_2_1_24_1","unstructured":"Gurobi Optimization. {n. d.}. Gurobi Optimizer. https:\/\/gurobi.com. Gurobi Optimization. {n. d.}. Gurobi Optimizer. https:\/\/gurobi.com."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"e_1_3_2_1_26_1","unstructured":"V. R. Royo D. Fridovich-Keil S. Herbert and C. J. Tomlin. 2018. Classification-based Approximate Reachability with Guarantees Applied to Safe Trajectory Tracking. arXiv preprint arXiv:1803.03237 (2018). V. R. Royo D. Fridovich-Keil S. Herbert and C. J. Tomlin. 2018. Classification-based Approximate Reachability with Guarantees Applied to Safe Trajectory Tracking. arXiv preprint arXiv:1803.03237 (2018)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"D. Silver A. Huang C. J. Maddison A. Guez etal 2016. Mastering the game of Go with deep neural networks and tree search. nature 529 7587 (2016) 484. D. Silver A. Huang C. J. Maddison A. Guez et al. 2016. Mastering the game of Go with deep neural networks and tree search. nature 529 7587 (2016) 484.","DOI":"10.1038\/nature16961"},{"key":"e_1_3_2_1_28_1","unstructured":"C. Szegedy W. Zaremba I. Sutskever J. Bruna D. Erhan etal 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013). C. Szegedy W. Zaremba I. Sutskever J. Bruna D. Erhan et al. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2014.220"},{"volume-title":"Quantifier elimination and cylindrical algebraic decomposition","author":"Tarski A.","key":"e_1_3_2_1_30_1","unstructured":"A. Tarski . 1998. A decision method for elementary algebra and geometry . In Quantifier elimination and cylindrical algebraic decomposition . Springer , 24--84. A. Tarski. 1998. A decision method for elementary algebra and geometry. In Quantifier elimination and cylindrical algebraic decomposition. Springer, 24--84."},{"key":"e_1_3_2_1_31_1","volume-title":"Benefits of depth in neural networks. arXiv preprint arXiv:1602.04485","author":"Telgarsky M.","year":"2016","unstructured":"M. Telgarsky . 2016. Benefits of depth in neural networks. arXiv preprint arXiv:1602.04485 ( 2016 ). M. Telgarsky. 2016. Benefits of depth in neural networks. arXiv preprint arXiv:1602.04485 (2016)."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3195970.3199852"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"R. J. Vanderbei etal 2015. Linear programming. Springer. R. J. Vanderbei et al. 2015. Linear programming. Springer.","DOI":"10.1007\/978-3-540-70529-1_419"},{"key":"e_1_3_2_1_34_1","author":"A","year":"1997","unstructured":"A . J. Wilkie. 1997 . Schanuel's conjecture and the decidability of the real exponential field. In Algebraic Model Theory. Springer, 223--230. A. J. Wilkie. 1997. Schanuel's conjecture and the decidability of the real exponential field. In Algebraic Model Theory. Springer, 223--230.","journal-title":"J. Wilkie."},{"key":"e_1_3_2_1_35_1","unstructured":"W. Xiang etal 2018. Verification for Machine Learning Autonomy and Neural Networks Survey. arXiv preprint arXiv:1810.01989 (2018). W. Xiang et al. 2018. Verification for Machine Learning Autonomy and Neural Networks Survey. arXiv preprint arXiv:1810.01989 (2018)."},{"key":"e_1_3_2_1_36_1","unstructured":"W. Xiang H. D. Tran and T. T. Johnson. 2017. Output reachable set estimation and verification for multi-layer neural networks. arXiv preprint arXiv:1708.03322 (2017). W. Xiang H. D. Tran and T. T. Johnson. 2017. Output reachable set estimation and verification for multi-layer neural networks. arXiv preprint arXiv:1708.03322 (2017)."},{"key":"e_1_3_2_1_37_1","unstructured":"C. Zhang S. Bengio M. Hardt B. Recht and O. Vinyals. 2016. Understanding deep learning requires rethinking generalization. arXiv preprint arXiv:1611.03530 (2016). C. Zhang S. Bengio M. Hardt B. Recht and O. Vinyals. 2016. Understanding deep learning requires rethinking generalization. arXiv preprint arXiv:1611.03530 (2016)."}],"event":{"name":"HSCC '19: 22nd ACM International Conference on Hybrid Systems: Computation and Control","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems"],"location":"Montreal Quebec Canada","acronym":"HSCC '19"},"container-title":["Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3302504.3311806","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3302504.3311806","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,8]],"date-time":"2023-09-08T10:21:44Z","timestamp":1694168504000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3302504.3311806"}},"subtitle":["verifying safety properties of hybrid systems with neural network controllers"],"short-title":[],"issued":{"date-parts":[[2019,4,16]]},"references-count":37,"alternative-id":["10.1145\/3302504.3311806","10.1145\/3302504"],"URL":"https:\/\/doi.org\/10.1145\/3302504.3311806","relation":{},"subject":[],"published":{"date-parts":[[2019,4,16]]},"assertion":[{"value":"2019-04-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}