{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:17Z","timestamp":1751662877658,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,8,24]],"date-time":"2021-08-24T00:00:00Z","timestamp":1629763200000},"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":[],"published-print":{"date-parts":[[2021,8,24]]},"DOI":"10.1145\/3476886.3477508","type":"proceedings-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T02:24:20Z","timestamp":1629339860000},"page":"42-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Building verified neural networks with specifications for systems"],"prefix":"10.1145","author":[{"given":"Cheng","family":"Tan","sequence":"first","affiliation":[{"name":"Bytedance Inc."}]},{"given":"Yibo","family":"Zhu","sequence":"additional","affiliation":[{"name":"ByteDance Inc."}]},{"given":"Chuanxiong","family":"Guo","sequence":"additional","affiliation":[{"name":"Bytedance Inc."}]}],"member":"320","published-online":{"date-parts":[[2021,8,24]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"competition for neural network verification (VNN-COMP). https:\/\/sites.google.com\/view\/vnn20\/vnncomp.  competition for neural network verification (VNN-COMP). https:\/\/sites.google.com\/view\/vnn20\/vnncomp."},{"key":"e_1_3_2_1_2_1","unstructured":"Neuralverification.jl. https:\/\/github.com\/sisl\/NeuralVerification.jl.  Neuralverification.jl. https:\/\/github.com\/sisl\/NeuralVerification.jl."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.inffus.2019.12.012"},{"key":"e_1_3_2_1_4_1","volume-title":"A unified view of piecewise linear neural network verification. arXiv preprint arXiv:1711.00455","author":"Bunel R.","year":"2017","unstructured":"R. Bunel , I. Turkaslan , P. H. Torr , P. Kohli , and M. P. Kumar . A unified view of piecewise linear neural network verification. arXiv preprint arXiv:1711.00455 , 2017 . R. Bunel, I. Turkaslan, P. H. Torr, P. Kohli, and M. P. Kumar. A unified view of piecewise linear neural network verification. arXiv preprint arXiv:1711.00455, 2017."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM42981.2021.9488898"},{"key":"e_1_3_2_1_6_1","volume-title":"41st International convention on information and communication technology, electronics and microelectronics (MIPRO)","author":"Do F. K.","year":"2018","unstructured":"F. K. Do šilovi\u0107, M. Br\u010di\u0107 , and N. Hlupi\u0107 . Explainable artificial intelligence: A survey. In 2018 41st International convention on information and communication technology, electronics and microelectronics (MIPRO) , 2018 . F. K. Došilovi\u0107, M. Br\u010di\u0107, and N. Hlupi\u0107. Explainable artificial intelligence: A survey. In 2018 41st International convention on information and communication technology, electronics and microelectronics (MIPRO), 2018."},{"key":"e_1_3_2_1_7_1","volume-title":"International Conference on Machine Learning","author":"Hashemi M.","year":"2018","unstructured":"M. Hashemi , K. Swersky , J. Smith , G. Ayers , H. Litz , J. Chang , C. Kozyrakis , and P. Ranganathan . Learning memory access patterns . In International Conference on Machine Learning , 2018 . M. Hashemi, K. Swersky, J. Smith, G. Ayers, H. Litz, J. Chang, C. Kozyrakis, and P. Ranganathan. Learning memory access patterns. In International Conference on Machine Learning, 2018."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341216.3342218"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196909"},{"key":"e_1_3_2_1_11_1","volume-title":"Learning to optimize join queries with deep reinforcement learning. arXiv preprint arXiv:1808.03196","author":"Krishnan S.","year":"2018","unstructured":"S. Krishnan , Z. Yang , K. Goldberg , J. Hellerstein , and I. Stoica . Learning to optimize join queries with deep reinforcement learning. arXiv preprint arXiv:1808.03196 , 2018 . S. Krishnan, Z. Yang, K. Goldberg, J. Hellerstein, and I. Stoica. Learning to optimize join queries with deep reinforcement learning. arXiv preprint arXiv:1808.03196, 2018."},{"key":"e_1_3_2_1_12_1","volume-title":"Algorithms for verifying deep neural networks. arXiv:1903.06758","author":"Liu C.","year":"2019","unstructured":"C. Liu , T. Arnon , C. Lazarus , C. Barrett , and M. J. Kochenderfer . Algorithms for verifying deep neural networks. arXiv:1903.06758 , 2019 . C. Liu, T. Arnon, C. Lazarus, C. Barrett, and M. J. Kochenderfer. Algorithms for verifying deep neural networks. arXiv:1903.06758, 2019."},{"key":"e_1_3_2_1_13_1","volume-title":"An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351","author":"Lomuscio A.","year":"2017","unstructured":"A. Lomuscio and L. Maganti . An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 , 2017 . A. Lomuscio and L. Maganti. An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351, 2017."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378525"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342080"},{"key":"e_1_3_2_1_16_1","volume-title":"Neural network robustness verification on gpus. arXiv preprint arXiv:2007.10868","author":"C.","year":"2020","unstructured":"C. Müller, G. Singh , M. Püschel, and M. Vechev . Neural network robustness verification on gpus. arXiv preprint arXiv:2007.10868 , 2020 . C. Müller, G. Singh, M. Püschel, and M. Vechev. Neural network robustness verification on gpus. arXiv preprint arXiv:2007.10868, 2020."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132785"},{"key":"e_1_3_2_1_18_1","volume-title":"Towards practical verification of machine learning: The case of computer vision systems. arXiv preprint arXiv:1712.01785","author":"Pei K.","year":"2017","unstructured":"K. Pei , Y. Cao , J. Yang , and S. Jana . Towards practical verification of machine learning: The case of computer vision systems. arXiv preprint arXiv:1712.01785 , 2017 . K. Pei, Y. Cao, J. Yang, and S. Jana. Towards practical verification of machine learning: The case of computer vision systems. arXiv preprint arXiv:1712.01785, 2017."},{"issue":"3","key":"e_1_3_2_1_19_1","first-page":"425","article-title":"Never: a tool for artificial neural networks verification","volume":"62","author":"Pulina L.","year":"2011","unstructured":"L. Pulina and A. Tacchella . Never: a tool for artificial neural networks verification . Annals of Mathematics and Artificial Intelligence , 62 ( 3 ):403– 425 , 2011 . L. Pulina and A. Tacchella. Never: a tool for artificial neural networks verification. Annals of Mathematics and Artificial Intelligence, 62(3):403–425, 2011.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229543.3229554"},{"key":"e_1_3_2_1_21_1","volume-title":"Learning to design circuits. arXiv preprint arXiv:1812.02734","author":"Wang H.","year":"2018","unstructured":"H. Wang , J. Yang , H.-S. Lee , and S. Han . Learning to design circuits. arXiv preprint arXiv:1812.02734 , 2018 . H. Wang, J. Yang, H.-S. Lee, and S. Han. Learning to design circuits. arXiv preprint arXiv:1812.02734, 2018."},{"key":"e_1_3_2_1_22_1","volume-title":"Proc. USENIX Security","author":"Wang S.","year":"2018","unstructured":"S. Wang , K. Pei , J. Whitehouse , J. Yang , and S. Jana . Formal security analysis of neural networks using symbolic intervals . In Proc. USENIX Security , 2018 . S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana. Formal security analysis of neural networks using symbolic intervals. In Proc. USENIX Security, 2018."},{"key":"e_1_3_2_1_23_1","volume-title":"Reachable set computation and safety verification for neural networks with relu activations. arXiv preprint arXiv:1712.08163","author":"Xiang W.","year":"2017","unstructured":"W. Xiang , H.-D. Tran , and T. T. Johnson . Reachable set computation and safety verification for neural networks with relu activations. arXiv preprint arXiv:1712.08163 , 2017 . W. Xiang, H.-D. Tran, and T. T. Johnson. Reachable set computation and safety verification for neural networks with relu activations. arXiv preprint arXiv:1712.08163, 2017."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2962027"}],"event":{"name":"APSys '21: 12th ACM SIGOPS Asia-Pacific Workshop on Systems","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Hong Kong China","acronym":"APSys '21"},"container-title":["Proceedings of the 12th ACM SIGOPS Asia-Pacific Workshop on Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3476886.3477508","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3476886.3477508","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:45Z","timestamp":1750188645000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3476886.3477508"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,24]]},"references-count":24,"alternative-id":["10.1145\/3476886.3477508","10.1145\/3476886"],"URL":"https:\/\/doi.org\/10.1145\/3476886.3477508","relation":{},"subject":[],"published":{"date-parts":[[2021,8,24]]},"assertion":[{"value":"2021-08-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}