{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T06:44:25Z","timestamp":1773384265177,"version":"3.50.1"},"publisher-location":"Cham","reference-count":76,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995232","type":"print"},{"value":"9783030995249","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex relaxation which over-approximates the non-convex activation functions, we encode the violations of activation functions as a cost function and optimize it with respect to the convex relaxation. The cost function, referred to as the Sum-of-Infeasibilities (SoI), is designed so that its minimum is zero and achieved only if all the activation functions are satisfied. We propose a stochastic procedure, , to efficiently minimize the SoI. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with . Extending the complete search with  achieves multiple simultaneous goals: 1) it guides the search towards a counter-example; 2) it enables more informed branching decisions; and 3) it creates additional opportunities for bound derivation. An extensive evaluation across different benchmarks and solvers demonstrates the benefit of the proposed techniques. In particular, we demonstrate that SoI significantly improves the performance of an existing complete search procedure. Moreover, the SoI-based implementation outperforms other state-of-the-art complete verifiers. We also show that our technique can efficiently improve upon the perturbation bound derived by a recent adversarial attack algorithm.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_8","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"143-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Efficient Neural Network Analysis with Sum-of-Infeasibilities"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5077-144X","authenticated-orcid":false,"given":"Haoze","family":"Wu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0673-9327","authenticated-orcid":false,"given":"Aleksandar","family":"Zelji\u0107","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5292-801X","authenticated-orcid":false,"given":"Guy","family":"Katz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: A synergistic approach for analyzing neural network robustness. In: Proc. Programming Language Design and Implementation (PLDI). p. 731\u2013744 (2019)","DOI":"10.1145\/3314221.3314614"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, R., Huchette, J., Ma, W., Tjandraatmadja, C., Vielma, J.P.: Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming pp. 1\u201337 (2020)","DOI":"10.1007\/s10107-020-01474-5"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Andrieu, C., De\u00a0Freitas, N., Doucet, A., Jordan, M.I.: An introduction to mcmc for machine learning. Machine learning 50(1), 5\u201343 (2003)","DOI":"10.1023\/A:1020281327116"},{"key":"8_CR4","unstructured":"Bak, S., Liu, C., Johnson, T.: The second international verification of neural networks competition (vnn-comp 2021): Summary and results. arXiv preprint arXiv:2109.00498 (2021)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Bak, S., Tran, H.D., Hobbs, K., Johnson, T.T.: Improved geometric path enumeration for verifying relu neural networks. In: International Conference on Computer Aided Verification. pp. 66\u201396. Springer (2020)","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"B\u00e9nichou, M., Gauthier, J.M., Girodet, P., Hentges, G., Ribi\u00e8re, G., Vincent, O.: Experiments in mixed-integer linear programming. Mathematical Programming 1(1), 76\u201394 (1971)","DOI":"10.1007\/BF01584074"},{"key":"8_CR7","unstructured":"Bojarski, M., Del\u00a0Testa, D., Dworakowski, D., Firner, B., Flepp, B., Goyal, P., Jackel, L.D., Monfort, M., Muller, U., Zhang, J., et\u00a0al.: End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Boopathy, A., Weng, T.W., Chen, P.Y., Liu, S., Daniel, L.: Cnn-cert: An efficient framework for certifying robustness of convolutional neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol.\u00a033, pp. 3240\u20133247 (2019)","DOI":"10.1609\/aaai.v33i01.33013240"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient verification of relu-based neural networks via dependency analysis. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol.\u00a034, pp. 3291\u20133299 (2020)","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Boyd, S., Boyd, S.P., Vandenberghe, L.: Convex optimization. Cambridge university press (2004)","DOI":"10.1017\/CBO9780511804441"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Brooks, S., Gelman, A., Jones, G., Meng, X.L.: Handbook of markov chain monte carlo. CRC press (2011)","DOI":"10.1201\/b10905"},{"key":"8_CR12","unstructured":"Bunel, R., De\u00a0Palma, A., Desmaison, A., Dvijotham, K., Kohli, P., Torr, P., Kumar, M.P.: Lagrangian decomposition for neural network verification. In: Conference on Uncertainty in Artificial Intelligence. pp. 370\u2013379. PMLR (2020)"},{"key":"8_CR13","unstructured":"Bunel, R., Lu, J., Turkaslan, I., Kohli, P., Torr, P., Mudigonda, P.: Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research 21(2020) (2020)"},{"key":"8_CR14","unstructured":"Bunel, R.R., Turkaslan, I., Torr, P., Kohli, P., Mudigonda, P.K.: A unified view of piecewise linear neural network verification. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems. vol.\u00a031. Curran Associates, Inc. (2018), https:\/\/proceedings.neurips.cc\/paper\/2018\/file\/be53d253d6bc3258a8160556dda3e9b2-Paper.pdf"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Carlini, N., Wagner, D.: Towards evaluating the robustness of neural networks. In: 2017 ieee symposium on security and privacy (sp). pp. 39\u201357. IEEE (2017)","DOI":"10.1109\/SP.2017.49"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Chib, S., Greenberg, E.: Understanding the metropolis-hastings algorithm. The american statistician 49(4), 327\u2013335 (1995)","DOI":"10.1080\/00031305.1995.10476177"},{"key":"8_CR17","unstructured":"Croce, F., Hein, M.: Reliable evaluation of adversarial robustness with an ensemble of diverse parameter-free attacks. In: International conference on machine learning. pp. 2206\u20132216. PMLR (2020)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Dantzig, G.B., Orden, A., Wolfe, P., et\u00a0al.: The generalized simplex method for minimizing a linear form under linear inequality restraints. Pacific Journal of Mathematics 5(2), 183\u2013195 (1955)","DOI":"10.2140\/pjm.1955.5.183"},{"key":"8_CR19","unstructured":"De\u00a0Palma, A., Behl, H., Bunel, R.R., Torr, P., Kumar, M.P.: Scaling the convex barrier with active sets. In: International Conference on Learning Representations (2020)"},{"key":"8_CR20","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings (2018)"},{"key":"8_CR21","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. In: UAI. vol.\u00a01, p.\u00a03 (2018)"},{"key":"8_CR22","unstructured":"Dvijotham, K.D., Stanforth, R., Gowal, S., Qin, C., De, S., Kohli, P.: Efficient neural network verification with exactness characterization. In: Uncertainty in Artificial Intelligence. pp. 497\u2013507. PMLR (2020)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: International Symposium on Automated Technology for Verification and Analysis. pp. 269\u2013286. Springer (2017)","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"8_CR24","unstructured":"Fischetti, M., Jo, J.: Deep neural networks as 0-1 mixed integer linear programs: A feasibility study. CoRR abs\/1712.06174 (2017)"},{"key":"8_CR25","unstructured":"Fromherz, A., Leino, K., Fredrikson, M., Parno, B., P\u0103s\u0103reanu, C.: Fast geometric projections for local robustness certification. arXiv preprint arXiv:2002.04742 (2020)"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA. pp. 3\u201318 (2018). https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"8_CR27","unstructured":"Gent, I.P., IRST, T.: Hybrid problems, hybrid solutions 73 j. hallam et al.(eds.) ios press, 1995 unsatisfied variables in local search. Hybrid problems, hybrid solutions 27, 73 (1995)"},{"key":"8_CR28","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572 (2014)"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Henriksen, P., Lomuscio, A.: Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In: Zhou, Z.H. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. pp. 2549\u20132555. International Joint Conferences on Artificial Intelligence Organization (8 2021). https:\/\/doi.org\/10.24963\/ijcai.2021\/351, main Track","DOI":"10.24963\/ijcai.2021\/351"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Hinton, G., Deng, L., Yu, D., Dahl, G.E., Mohamed, A.r., Jaitly, N., Senior, A., Vanhoucke, V., Nguyen, P., Sainath, T.N., et\u00a0al.: Deep neural networks for acoustic modeling in speech recognition: The shared views of four research groups. IEEE Signal processing magazine 29(6), 82\u201397 (2012)","DOI":"10.1109\/MSP.2012.2205597"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: CAV (2017)","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"8_CR32","unstructured":"Jia, Z., Zaharia, M., Aiken, A.: Beyond data and model parallelism for deep neural networks. In: Talwalkar, A., Smith, V., Zaharia, M. (eds.) Proceedings of Machine Learning and Systems. vol.\u00a01, pp. 1\u201313 (2019), https:\/\/proceedings.mlsys.org\/paper\/2019\/file\/c74d97b01eae257e44aa9d5bade97baf-Paper.pdf"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Julian, K.D., Lee, R., Kochenderfer, M.J.: Validation of image-based neural network controllers through adaptive stress testing. In: 2020 IEEE 23rd International Conference on Intelligent Transportation Systems (ITSC). pp.\u00a01\u20137. IEEE (2020)","DOI":"10.1109\/ITSC45102.2020.9294549"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Kass, R.E., Carlin, B.P., Gelman, A., Neal, R.M.: Markov chain monte carlo in practice: a roundtable discussion. The American Statistician 52(2), 93\u2013100 (1998)","DOI":"10.1080\/00031305.1998.10480547"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Proc. 29th Int. Conf. on Computer Aided Verification (CAV). pp. 97\u2013117 (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zelji\u0107, A., et\u00a0al.: The marabou framework for verification and analysis of deep neural networks. In: International Conference on Computer Aided Verification. pp. 443\u2013452 (2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Khedr, H., Ferlez, J., Shoukry, Y.: Peregrinn: Penalized-relaxation greedy neural network verifier. arXiv preprint arXiv:2006.10864 (2020)","DOI":"10.1007\/978-3-030-81685-8_13"},{"key":"8_CR38","unstructured":"King, T.: Effective algorithms for the satisfiability of quantifier-free formulas over linear real and integer arithmetic. Ph.D. thesis, Citeseer (2014)"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"King, T., Barrett, C., Dutertre, B.: Simplex with sum of infeasibilities for smt. In: 2013 Formal Methods in Computer-Aided Design. pp. 189\u2013196. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679409"},{"key":"8_CR40","unstructured":"Krizhevsky, A., Nair, V., Hinton, G.: Cifar-10 (canadian institute for advanced research). URL http:\/\/www.cs.toronto.edu\/kriz\/cifar.html\u00a05(4), 1 (2010)"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Kurakin, A., Goodfellow, I.J., Bengio, S.: Adversarial examples in the physical world. In: ICLR (Workshop). OpenReview.net (2017)","DOI":"10.1201\/9781351251389-8"},{"key":"8_CR42","unstructured":"LeCun, Y., Cortes, C.: MNIST handwritten digit database. http:\/\/yann.lecun.com\/exdb\/mnist\/ (2010), http:\/\/yann.lecun.com\/exdb\/mnist\/"},{"key":"8_CR43","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. arXiv preprint arXiv:1903.06758 (2019)"},{"key":"8_CR44","unstructured":"Lu, J., Kumar, M.P.: Neural network branching for neural network verification. arXiv preprint arXiv:1912.01329 (2019)"},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Lyu, Z., Ko, C.Y., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened crown: Tightened neural network robustness certificates. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol.\u00a034, pp. 5037\u20135044 (2020)","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"8_CR46","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083 (2017)"},{"key":"8_CR47","doi-asserted-by":"crossref","unstructured":"Masi, I., Wu, Y., Hassner, T., Natarajan, P.: Deep face recognition: A survey. In: 2018 31st SIBGRAPI conference on graphics, patterns and images (SIBGRAPI). pp. 471\u2013478. IEEE (2018)","DOI":"10.1109\/SIBGRAPI.2018.00067"},{"key":"8_CR48","unstructured":"M\u00fcller, C., Serre, F., Singh, G., P\u00fcschel, M., Vechev, M.: Scaling polyhedral neural network verification on gpus. Proceedings of Machine Learning and Systems 3 (2021)"},{"key":"8_CR49","unstructured":"M\u00fcller, M.N., Makarchuk, G., Singh, G., P\u00fcschel, M., Vechev, M.: Precise multi-neuron abstractions for neural network certification. arXiv preprint arXiv:2103.03638 (2021)"},{"key":"8_CR50","doi-asserted-by":"crossref","unstructured":"Paterson, C., Wu, H., Grese, J., Calinescu, R., Pasareanu, C.S., Barrett, C.: Deepcert: Verification of contextually relevant robustness for neural network image classifiers. arXiv preprint arXiv:2103.01629 (2021)","DOI":"10.1007\/978-3-030-83903-1_5"},{"key":"8_CR51","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.: Semidefinite relaxations for certifying robustness to adversarial examples. arXiv preprint arXiv:1811.01057 (2018)"},{"key":"8_CR52","unstructured":"Salman, H., Yang, G., Zhang, H., Hsieh, C.J., Zhang, P.: A convex relaxation barrier to tight robustness verification of neural networks. In: Wallach, H., Larochelle, H., Beygelzimer, A., d\u2019Alch\u00e9-Buc, F., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems. vol.\u00a032. Curran Associates, Inc. (2019), https:\/\/proceedings.neurips.cc\/paper\/2019\/file\/246a3c5544feb054f3ea718f61adfa16-Paper.pdf"},{"key":"8_CR53","doi-asserted-by":"crossref","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. ACM SIGARCH Computer Architecture News 41(1), 305\u2013316 (2013)","DOI":"10.1145\/2490301.2451150"},{"key":"8_CR54","unstructured":"Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: AAAI. vol.\u00a094, pp. 337\u2013343 (1994)"},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"Silver, D., Huang, A., Maddison, C.J., Guez, A., Sifre, L., Van Den\u00a0Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., et\u00a0al.: Mastering the game of go with deep neural networks and tree search. nature 529(7587), 484 (2016)","DOI":"10.1038\/nature16961"},{"key":"8_CR56","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. Advances in Neural Information Processing Systems 32, 15098\u201315109 (2019)"},{"key":"8_CR57","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. Advances in Neural Information Processing Systems 31, 10802\u201310813 (2018)"},{"key":"8_CR58","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3(POPL), 1\u201330 (2019)","DOI":"10.1145\/3290354"},{"key":"8_CR59","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: Boosting robustness certification of neural networks. In: International Conference on Learning Representations (2019)"},{"key":"8_CR60","doi-asserted-by":"crossref","unstructured":"Stallkamp, J., Schlipsing, M., Salmen, J., Igel, C.: The german traffic sign recognition benchmark: a multi-class classification competition. In: The 2011 international joint conference on neural networks. pp. 1453\u20131460. IEEE (2011)","DOI":"10.1109\/IJCNN.2011.6033395"},{"key":"8_CR61","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)"},{"key":"8_CR62","unstructured":"Tjandraatmadja, C., Anderson, R., Huchette, J., Ma, W., PATEL, K.K., Vielma, J.P.: The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M.F., Lin, H. (eds.) Advances in Neural Information Processing Systems. vol.\u00a033, pp. 21675\u201321686. Curran Associates, Inc. (2020), https:\/\/proceedings.neurips.cc\/paper\/2020\/file\/f6c2a0c4b566bc99d596e58638e342b0-Paper.pdf"},{"key":"8_CR63","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net (2019), https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"8_CR64","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Bak, S., Xiang, W., Johnson, T.T.: Verification of deep convolutional neural networks using imagestars. In: International Conference on Computer Aided Verification. pp. 18\u201342. Springer (2020)","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"8_CR65","doi-asserted-by":"crossref","unstructured":"Vincent, J.A., Schwager, M.: Reachable polyhedral marching (rpm): A safety verification algorithm for robotic systems with deep neural network components. arXiv preprint arXiv:2011.11609 (2020)","DOI":"10.1109\/ICRA48506.2021.9561956"},{"key":"8_CR66","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montr\u00e9al, Canada. pp. 6369\u20136379 (2018), http:\/\/papers.nips.cc\/paper\/7873-efficient-formal-safety-analysis-of-neural-networks"},{"key":"8_CR67","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018. pp. 1599\u20131614 (2018), https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi"},{"key":"8_CR68","unstructured":"Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, J.Z.: Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624 (2021)"},{"key":"8_CR69","unstructured":"Weng, L., Zhang, H., Chen, H., Song, Z., Hsieh, C.J., Daniel, L., Boning, D., Dhillon, I.: Towards fast computation of certified robustness for relu networks. In: International Conference on Machine Learning. pp. 5276\u20135285. PMLR (2018)"},{"key":"8_CR70","unstructured":"Wong, E., Kolter, Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: International Conference on Machine Learning. pp. 5286\u20135295. PMLR (2018)"},{"key":"8_CR71","unstructured":"Wu, H., Ozdemir, A., Zelji\u0107, A., Julian, K., Irfan, A., Gopinath, D., Fouladi, S., Katz, G., Pasareanu, C., Barrett, C.: Parallelization techniques for verifying neural networks. In: 2020 Formal Methods in Computer Aided Design (FMCAD). pp. 128\u2013137. IEEE (2020)"},{"key":"8_CR72","unstructured":"Wu, H., Zelji\u0107, A., Katz, G., Barrett, C.: Artifact for Paper Efficient Neural Network Analysis with Sum-of-Infeasibilities (Feb 2022), https:\/\/doi.org\/10.5281\/zenodo.6109456"},{"key":"8_CR73","doi-asserted-by":"crossref","unstructured":"Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multilayer neural networks. IEEE transactions on neural networks and learning systems 29(11), 5777\u20135783 (2018)","DOI":"10.1109\/TNNLS.2018.2808470"},{"key":"8_CR74","unstructured":"Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K.W., Huang, M., Kailkhura, B., Lin, X., Hsieh, C.J.: Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems 33 (2020)"},{"key":"8_CR75","unstructured":"Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., Hsieh, C.J.: Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. arXiv preprint arXiv:2011.13824 (2020)"},{"key":"8_CR76","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems. vol.\u00a031. Curran Associates, Inc. (2018), https:\/\/proceedings.neurips.cc\/paper\/2018\/file\/d04863f100d59b3eb688a11f95b0ae60-Paper.pdf"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:18:00Z","timestamp":1648534680000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":76,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}