{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:40:09Z","timestamp":1774838409617,"version":"3.50.1"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["RINGS #2148583"],"award-info":[{"award-number":["RINGS #2148583"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>Recently, Graph Neural Networks (GNNs) have been applied for scheduling jobs over clusters, achieving better performance than hand-crafted heuristics. Despite their impressive performance, concerns remain over whether these GNN-based job schedulers meet users\u2019 expectations about other important properties, such as strategy-proofness, sharing incentive, and stability. In this work, we consider formal verification of GNN-based job schedulers. We address several domain-specific challenges such as networks that are deeper and specifications that are richer than those encountered when verifying image and NLP classifiers. We develop vegas, the first general framework for verifying both single-step and multi-step properties of these schedulers based on carefully designed algorithms that combine abstractions, refinements, solvers, and proof transfer. Our experimental results show that vegas achieves significant speed-up when verifying important properties of a state-of-the-art GNN-based scheduler compared to previous methods.<\/jats:p>","DOI":"10.1145\/3563325","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1036-1065","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Scalable verification of GNN-based job schedulers"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5077-144X","authenticated-orcid":false,"given":"Haoze","family":"Wu","sequence":"first","affiliation":[{"name":"Stanford University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7661-2220","authenticated-orcid":false,"given":"Mahmood","family":"Sharif","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5181-4560","authenticated-orcid":false,"given":"Nina","family":"Narodytska","sequence":"additional","affiliation":[{"name":"VMware Research, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9299-2961","authenticated-orcid":false,"given":"Gagandeep","family":"Singh","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Alfred V Aho Monica S Lam Ravi Sethi and Jeffrey D Ullman. 2007. Compilers: principles techniques & tools. Pearson Education India. \t\t\t\t  Alfred V Aho Monica S Lam Ravi Sethi and Jeffrey D Ullman. 2007. Compilers: principles techniques & tools. Pearson Education India."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_28"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314614"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01741-4","volume-title":"The datacenter as a computer: An introduction to the design of warehouse-scale machines. Synthesis lectures on computer architecture, 8, 3","author":"Barroso Luiz Andr\u00e9","year":"2013","unstructured":"Luiz Andr\u00e9 Barroso , Jimmy Clidaras , and Urs H\u00f6lzle . 2013. The datacenter as a computer: An introduction to the design of warehouse-scale machines. Synthesis lectures on computer architecture, 8, 3 ( 2013 ), 1\u2013154. Luiz Andr\u00e9 Barroso, Jimmy Clidaras, and Urs H\u00f6lzle. 2013. The datacenter as a computer: An introduction to the design of warehouse-scale machines. Synthesis lectures on computer architecture, 8, 3 (2013), 1\u2013154."},{"key":"e_1_2_1_6_1","unstructured":"Aleksandar Bojchevski and Stephan G\u00fcnnemann. 2019. Certifiable robustness to graph perturbations. arXiv preprint arXiv:1910.14356. \t\t\t\t  Aleksandar Bojchevski and Stephan G\u00fcnnemann. 2019. Certifiable robustness to graph perturbations. arXiv preprint arXiv:1910.14356."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33013240"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"e_1_2_1_9_1","article-title":"Branch and bound for piecewise linear neural network verification","volume":"21","author":"Bunel Rudy","year":"2020","unstructured":"Rudy Bunel , Jingyue Lu , Ilker Turkaslan , Pushmeet Kohli , P Torr , and P Mudigonda . 2020 . Branch and bound for piecewise linear neural network verification . Journal of Machine Learning Research , 21 , 2020 (2020). Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Pushmeet Kohli, P Torr, and P Mudigonda. 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21, 2020 (2020).","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_1_10_1","volume-title":"Advances in Neural Information Processing Systems","author":"Bunel Rudy R","year":"2018","unstructured":"Rudy R Bunel , Ilker Turkaslan , Philip Torr , Pushmeet Kohli , and Pawan K Mudigonda . 2018. A Unified View of Piecewise Linear Neural Network Verification . In Advances in Neural Information Processing Systems , S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.). 31, Curran Associates, Inc. . https:\/\/proceedings.neurips.cc\/paper\/ 2018 \/file\/be53d253d6bc3258a8160556dda3e9b2-Paper.pdf Rudy R Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda. 2018. A Unified View of Piecewise Linear Neural Network Verification. In Advances in Neural Information Processing Systems, S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.). 31, Curran Associates, Inc.. https:\/\/proceedings.neurips.cc\/paper\/2018\/file\/be53d253d6bc3258a8160556dda3e9b2-Paper.pdf"},{"key":"e_1_2_1_11_1","unstructured":"Hongkai Dai Benoit Landry Lujie Yang Marco Pavone and Russ Tedrake. 2021. Lyapunov-stable neural-network control. arXiv preprint arXiv:2109.14152. \t\t\t\t  Hongkai Dai Benoit Landry Lujie Yang Marco Pavone and Russ Tedrake. 2021. Lyapunov-stable neural-network control. arXiv preprint arXiv:2109.14152."},{"key":"e_1_2_1_12_1","volume-title":"Rudy Bunel, Philip HS Torr, and M Pawan Kumar.","author":"Palma Alessandro De","year":"2021","unstructured":"Alessandro De Palma , Harkirat Singh Behl , Rudy Bunel, Philip HS Torr, and M Pawan Kumar. 2021 . Scaling the convex barrier with active sets. arXiv preprint arXiv:2101.05844. Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip HS Torr, and M Pawan Kumar. 2021. Scaling the convex barrier with active sets. arXiv preprint arXiv:2101.05844."},{"key":"e_1_2_1_13_1","volume-title":"Convolutional neural networks on graphs with fast localized spectral filtering. Advances in neural information processing systems, 29","author":"Defferrard Micha\u00ebl","year":"2016","unstructured":"Micha\u00ebl Defferrard , Xavier Bresson , and Pierre Vandergheynst . 2016. Convolutional neural networks on graphs with fast localized spectral filtering. Advances in neural information processing systems, 29 ( 2016 ), https:\/\/doi.org\/10.5555\/3157382.3157527 10.5555\/3157382.3157527 Micha\u00ebl Defferrard, Xavier Bresson, and Pierre Vandergheynst. 2016. Convolutional neural networks on graphs with fast localized spectral filtering. Advances in neural information processing systems, 29 (2016), https:\/\/doi.org\/10.5555\/3157382.3157527"},{"key":"e_1_2_1_14_1","volume-title":"NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings.","author":"Dutta Souradeep","year":"2018","unstructured":"Souradeep Dutta , Susmit Jha , Sriram Sankaranarayanan , and Ashish Tiwari . 2018 . 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. Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. 2018. 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."},{"key":"e_1_2_1_15_1","volume-title":"Proc. Advances in Neural Information Processing Systems (NeurIPS), Corinna Cortes, Neil D","author":"Duvenaud David","unstructured":"David Duvenaud , Dougal Maclaurin , Jorge Aguilera-Iparraguirre , Rafael G\u00f3mez-Bombarelli , Timothy Hirzel , Al\u00e1n Aspuru-Guzik , and Ryan P. Adams . 2015. Convolutional Networks on Graphs for Learning Molecular Fingerprints . In Proc. Advances in Neural Information Processing Systems (NeurIPS), Corinna Cortes, Neil D . Lawrence, Daniel D. Lee, Masashi Sugiyama, and Roman Garnett (Eds.). 2224\u20132232. David Duvenaud, Dougal Maclaurin, Jorge Aguilera-Iparraguirre, Rafael G\u00f3mez-Bombarelli, Timothy Hirzel, Al\u00e1n Aspuru-Guzik, and Ryan P. Adams. 2015. Convolutional Networks on Graphs for Learning Molecular Fingerprints. In Proc. Advances in Neural Information Processing Systems (NeurIPS), Corinna Cortes, Neil D. Lawrence, Daniel D. Lee, Masashi Sugiyama, and Roman Garnett (Eds.). 2224\u20132232."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_2_1_17_1","volume-title":"Deep Neural Networks as 0-1 Mixed Integer Linear Programs: A Feasibility Study. CoRR, abs\/1712.06174","author":"Fischetti Matteo","year":"2017","unstructured":"Matteo Fischetti and Jason Jo. 2017. Deep Neural Networks as 0-1 Mixed Integer Linear Programs: A Feasibility Study. CoRR, abs\/1712.06174 ( 2017 ). Matteo Fischetti and Jason Jo. 2017. Deep Neural Networks as 0-1 Mixed Integer Linear Programs: A Feasibility Study. CoRR, abs\/1712.06174 (2017)."},{"key":"e_1_2_1_18_1","volume-title":"Proc. Advances in Neural Information Processing Systems (NeurIPS). 6530\u20136539","author":"Fout Alex","year":"2017","unstructured":"Alex Fout , Jonathon Byrd , Basir Shariat , and Asa Ben-Hur . 2017 . Protein Interface Prediction using Graph Convolutional Networks . In Proc. Advances in Neural Information Processing Systems (NeurIPS). 6530\u20136539 . Alex Fout, Jonathon Byrd, Basir Shariat, and Asa Ben-Hur. 2017. Protein Interface Prediction using Graph Convolutional Networks. In Proc. Advances in Neural Information Processing Systems (NeurIPS). 6530\u20136539."},{"key":"e_1_2_1_19_1","unstructured":"Aymeric Fromherz Klas Leino Matt Fredrikson Bryan Parno and Corina P\u0103s\u0103reanu. 2020. Fast geometric projections for local robustness certification. arXiv preprint arXiv:2002.04742. \t\t\t\t  Aymeric Fromherz Klas Leino Matt Fredrikson Bryan Parno and Corina P\u0103s\u0103reanu. 2020. Fast geometric projections for local robustness certification. arXiv preprint arXiv:2002.04742."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_2_1_21_1","volume-title":"8th USENIX Symposium on Networked Systems Design and Implementation (NSDI 11)","author":"Ghodsi Ali","year":"2011","unstructured":"Ali Ghodsi , Matei Zaharia , Benjamin Hindman , Andy Konwinski , Scott Shenker , and Ion Stoica . 2011 . Dominant resource fairness: Fair allocation of multiple resource types . In 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI 11) . https:\/\/doi.org\/10.5555\/1972457.1972490 10.5555\/1972457.1972490 Ali Ghodsi, Matei Zaharia, Benjamin Hindman, Andy Konwinski, Scott Shenker, and Ion Stoica. 2011. Dominant resource fairness: Fair allocation of multiple resource types. In 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI 11). https:\/\/doi.org\/10.5555\/1972457.1972490"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2021\/351"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Xiaowei Huang Marta Kwiatkowska Sen Wang and Min Wu. 2017. Safety Verification of Deep Neural Networks. In CAV. \t\t\t\t  Xiaowei Huang Marta Kwiatkowska Sen Wang and Min Wu. 2017. Safety Verification of Deep Neural Networks. In CAV.","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_2_1_24_1","unstructured":"Kirthevasan Kandasamy Gur-Eyal Sela Joseph E Gonzalez Michael I Jordan and Ion Stoica. 2020. Online learning demands in max-min fairness. arXiv preprint arXiv:2012.08648. \t\t\t\t  Kirthevasan Kandasamy Gur-Eyal Sela Joseph E Gonzalez Michael I Jordan and Ion Stoica. 2020. Online learning demands in max-min fairness. arXiv preprint arXiv:2012.08648."},{"key":"e_1_2_1_25_1","volume-title":"Proc. 29th Int. Conf. on Computer Aided Verification (CAV). 97\u2013117","author":"Katz G.","unstructured":"G. Katz , C. Barrett , D. Dill , K. Julian , and M. Kochenderfer . 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks . In Proc. 29th Int. Conf. on Computer Aided Verification (CAV). 97\u2013117 . G. Katz, C. Barrett, D. Dill, K. Julian, and M. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Proc. 29th Int. Conf. on Computer Aided Verification (CAV). 97\u2013117."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_2_1_27_1","volume-title":"Learning combinatorial optimization algorithms over graphs. Advances in neural information processing systems, 30","author":"Khalil Elias","year":"2017","unstructured":"Elias Khalil , Hanjun Dai , Yuyu Zhang , Bistra Dilkina , and Le Song . 2017. Learning combinatorial optimization algorithms over graphs. Advances in neural information processing systems, 30 ( 2017 ), https:\/\/doi.org\/10.5555\/3295222.3295382 10.5555\/3295222.3295382 Elias Khalil, Hanjun Dai, Yuyu Zhang, Bistra Dilkina, and Le Song. 2017. Learning combinatorial optimization algorithms over graphs. Advances in neural information processing systems, 30 (2017), https:\/\/doi.org\/10.5555\/3295222.3295382"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Haitham Khedr James Ferlez and Yasser Shoukry. 2020. PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier. arXiv preprint arXiv:2006.10864. \t\t\t\t  Haitham Khedr James Ferlez and Yasser Shoukry. 2020. PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier. arXiv preprint arXiv:2006.10864.","DOI":"10.1007\/978-3-030-81685-8_13"},{"key":"e_1_2_1_29_1","volume-title":"Proc. International Conference on Learning Representations, (ICLR). OpenReview.net.","author":"Thomas","unstructured":"Thomas N. Kipf and Max Welling. 2017. Semi-Supervised Classification with Graph Convolutional Networks . In Proc. International Conference on Learning Representations, (ICLR). OpenReview.net. Thomas N. Kipf and Max Welling. 2017. Semi-Supervised Classification with Graph Convolutional Networks. In Proc. International Conference on Learning Representations, (ICLR). OpenReview.net."},{"key":"e_1_2_1_30_1","unstructured":"Yann LeCun and Corinna Cortes. 2010. MNIST handwritten digit database. http:\/\/yann.lecun.com\/exdb\/mnist\/. http:\/\/yann.lecun.com\/exdb\/mnist\/ \t\t\t\t  Yann LeCun and Corinna Cortes. 2010. MNIST handwritten digit database. http:\/\/yann.lecun.com\/exdb\/mnist\/. http:\/\/yann.lecun.com\/exdb\/mnist\/"},{"key":"e_1_2_1_31_1","unstructured":"Jingyue Lu and M Pawan Kumar. 2019. Neural network branching for neural network verification. arXiv preprint arXiv:1912.01329. \t\t\t\t  Jingyue Lu and M Pawan Kumar. 2019. Neural network branching for neural network verification. arXiv preprint arXiv:1912.01329."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342080"},{"key":"e_1_2_1_34_1","first-page":"3","volume-title":"Proceedings of Machine Learning and Systems","author":"M\u00fcller Christoph","year":"2021","unstructured":"Christoph M\u00fcller , Fran\u00e7ois Serre , Gagandeep Singh , Markus P\u00fcschel , and Martin Vechev . 2021 . Scaling Polyhedral Neural Network Verification on GPUs . Proceedings of Machine Learning and Systems , 3 (2021). Christoph M\u00fcller, Fran\u00e7ois Serre, Gagandeep Singh, Markus P\u00fcschel, and Martin Vechev. 2021. Scaling Polyhedral Neural Network Verification on GPUs. Proceedings of Machine Learning and Systems, 3 (2021)."},{"key":"e_1_2_1_35_1","unstructured":"Mark Niklas M\u00fcller Gleb Makarchuk Gagandeep Singh Markus P\u00fcschel and Martin Vechev. 2021. Precise Multi-Neuron Abstractions for Neural Network Certification. arXiv preprint arXiv:2103.03638. \t\t\t\t  Mark Niklas M\u00fcller Gleb Makarchuk Gagandeep Singh Markus P\u00fcschel and Martin Vechev. 2021. Precise Multi-Neuron Abstractions for Neural Network Certification. arXiv preprint arXiv:2103.03638."},{"key":"e_1_2_1_36_1","first-page":"2014","article-title":"Learning Convolutional Neural Networks for Graphs. In Proc. International Conference on Machine Learning","volume":"48","author":"Niepert Mathias","year":"2016","unstructured":"Mathias Niepert , Mohamed Ahmed , and Konstantin Kutzkov . 2016 . Learning Convolutional Neural Networks for Graphs. In Proc. International Conference on Machine Learning , ICML. 48 , 2014 \u2013 2023 . Mathias Niepert, Mohamed Ahmed, and Konstantin Kutzkov. 2016. Learning Convolutional Neural Networks for Graphs. In Proc. International Conference on Machine Learning, ICML. 48, 2014\u20132023.","journal-title":"ICML."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207543.2020.1870013"},{"key":"e_1_2_1_38_1","unstructured":"Aditi Raghunathan Jacob Steinhardt and Percy Liang. 2018. Semidefinite relaxations for certifying robustness to adversarial examples. arXiv preprint arXiv:1811.01057. \t\t\t\t  Aditi Raghunathan Jacob Steinhardt and Percy Liang. 2018. Semidefinite relaxations for certifying robustness to adversarial examples. arXiv preprint arXiv:1811.01057."},{"key":"e_1_2_1_39_1","volume-title":"Scalable Polyhedral Verification of Recurrent Neural Networks. In International Conference on Computer Aided Verification. 225\u2013248","author":"Ryou Wonryong","year":"2021","unstructured":"Wonryong Ryou , Jiayu Chen , Mislav Balunovic , Gagandeep Singh , Andrei Dan , and Martin Vechev . 2021 . Scalable Polyhedral Verification of Recurrent Neural Networks. In International Conference on Computer Aided Verification. 225\u2013248 . Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh, Andrei Dan, and Martin Vechev. 2021. Scalable Polyhedral Verification of Recurrent Neural Networks. In International Conference on Computer Aided Verification. 225\u2013248."},{"key":"e_1_2_1_40_1","volume-title":"Advances in Neural Information Processing Systems, H. Wallach, H. Larochelle, A. Beygelzimer, F. d' Alch\u00e9-Buc","author":"Salman Hadi","year":"2019","unstructured":"Hadi Salman , Greg Yang , Huan Zhang , Cho-Jui Hsieh , and Pengchuan Zhang . 2019. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks . In Advances in Neural Information Processing Systems, H. Wallach, H. Larochelle, A. Beygelzimer, F. d' Alch\u00e9-Buc , E. Fox, and R. Garnett (Eds.). 32, Curran Associates, Inc. . https:\/\/proceedings.neurips.cc\/paper\/ 2019 \/file\/246a3c5544feb054f3ea718f61adfa16-Paper.pdf Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. 2019. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. In Advances in Neural Information Processing Systems, H. Wallach, H. Larochelle, A. Beygelzimer, F. d' Alch\u00e9-Buc, E. Fox, and R. Garnett (Eds.). 32, Curran Associates, Inc.. https:\/\/proceedings.neurips.cc\/paper\/2019\/file\/246a3c5544feb054f3ea718f61adfa16-Paper.pdf"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465351.2465387"},{"key":"e_1_2_1_42_1","first-page":"15098","article-title":"Beyond the single neuron convex barrier for neural network certification","volume":"32","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh , Rupanshu Ganvir , Markus P\u00fcschel , and Martin Vechev . 2019 . Beyond the single neuron convex barrier for neural network certification . Advances in Neural Information Processing Systems , 32 (2019), 15098 \u2013 15109 . Gagandeep Singh, Rupanshu Ganvir, Markus P\u00fcschel, and Martin Vechev. 2019. Beyond the single neuron convex barrier for neural network certification. Advances in Neural Information Processing Systems, 32 (2019), 15098\u201315109.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_2_1_43_1","first-page":"10802","article-title":"Fast and effective robustness certification","volume":"31","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh , Timon Gehr , Matthew Mirman , Markus P\u00fcschel , and Martin Vechev . 2018 . Fast and effective robustness certification . Advances in Neural Information Processing Systems , 31 (2018), 10802 \u2013 10813 . Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P\u00fcschel, and Martin Vechev. 2018. Fast and effective robustness certification. Advances in Neural Information Processing Systems, 31 (2018), 10802\u201310813.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_2_1_45_1","volume-title":"Boosting Robustness Certification of Neural Networks. In International Conference on Learning Representations.","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh , Timon Gehr , Markus P\u00fcschel , and Martin Vechev . 2019 . Boosting Robustness Certification of Neural Networks. In International Conference on Learning Representations. Gagandeep Singh, Timon Gehr, Markus P\u00fcschel, and Martin Vechev. 2019. Boosting Robustness Certification of Neural Networks. In International Conference on Learning Representations."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_2_1_47_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh , Markus P\u00fcschel , and Martin T. Vechev . 2018. A practical construction for decomposing numerical abstract domains . Proc. ACM Program. Lang., 2, POPL ( 2018 ), 55:1\u201355:28. Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2018. A practical construction for decomposing numerical abstract domains. Proc. ACM Program. Lang., 2, POPL (2018), 55:1\u201355:28."},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence. 3314\u20133320","author":"Sun Penghao","year":"2021","unstructured":"Penghao Sun , Zehua Guo , Junchao Wang , Junfei Li , Julong Lan , and Yuxiang Hu . 2021 . Deepweave: Accelerating job completion time with deep reinforcement learning-based coflow scheduling . In Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence. 3314\u20133320 . https:\/\/doi.org\/10.5555\/3491440.3491898 10.5555\/3491440.3491898 Penghao Sun, Zehua Guo, Junchao Wang, Junfei Li, Julong Lan, and Yuxiang Hu. 2021. Deepweave: Accelerating job completion time with deep reinforcement learning-based coflow scheduling. In Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence. 3314\u20133320. https:\/\/doi.org\/10.5555\/3491440.3491898"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311802"},{"key":"e_1_2_1_50_1","unstructured":"Christian Szegedy Wojciech Zaremba Ilya Sutskever Joan Bruna Dumitru Erhan Ian Goodfellow and Rob Fergus. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199. \t\t\t\t  Christian Szegedy Wojciech Zaremba Ilya Sutskever Joan Bruna Dumitru Erhan Ian Goodfellow and Rob Fergus. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199."},{"key":"e_1_2_1_51_1","volume-title":"KRUNAL KISHOR PATEL, and Juan Pablo Vielma","author":"Tjandraatmadja Christian","year":"2020","unstructured":"Christian Tjandraatmadja , Ross Anderson , Joey Huchette , Will Ma , KRUNAL KISHOR PATEL, and Juan Pablo Vielma . 2020 . The Convex Relaxation Barrier, Revisited : Tightened Single-Neuron Relaxations for Neural Network Verification. In Advances in Neural Information Processing Systems, H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin (Eds.). 33, Curran Associates, Inc ., 21675\u201321686. https:\/\/proceedings.neurips.cc\/paper\/2020\/file\/f6c2a0c4b566bc99d596e58638e342b0-Paper.pdf Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, KRUNAL KISHOR PATEL, and Juan Pablo Vielma. 2020. The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification. In Advances in Neural Information Processing Systems, H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin (Eds.). 33, Curran Associates, Inc., 21675\u201321686. https:\/\/proceedings.neurips.cc\/paper\/2020\/file\/f6c2a0c4b566bc99d596e58638e342b0-Paper.pdf"},{"key":"e_1_2_1_52_1","volume-title":"Evaluating Robustness of Neural Networks with Mixed Integer Programming. In 7th International Conference on Learning Representations, ICLR 2019","author":"Tjeng Vincent","year":"2019","unstructured":"Vincent Tjeng , Kai Y. Xiao , and Russ Tedrake . 2019 . 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. https:\/\/openreview.net\/forum?id=HyGIdiRqtm Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. 2019. 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. https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428253"},{"key":"e_1_2_1_55_1","doi-asserted-by":"crossref","unstructured":"Joseph A Vincent and Mac Schwager. 2020. Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components. arXiv preprint arXiv:2011.11609. \t\t\t\t  Joseph A Vincent and Mac Schwager. 2020. Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components. arXiv preprint arXiv:2011.11609.","DOI":"10.1109\/ICRA48506.2021.9561956"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3447548.3467295"},{"key":"e_1_2_1_57_1","volume-title":"Proc. International Joint Conference on Artificial Intelligence, (IJCAI). 3762\u20133770","author":"Wang Shen","unstructured":"Shen Wang , Zhengzhang Chen , Xiao Yu , Ding Li , Jingchao Ni , Lu-An Tang , Jiaping Gui , Zhichun Li , Haifeng Chen , and Philip S. Yu . 2019. Heterogeneous Graph Matching Networks for Unknown Malware Detection . In Proc. International Joint Conference on Artificial Intelligence, (IJCAI). 3762\u20133770 . Shen Wang, Zhengzhang Chen, Xiao Yu, Ding Li, Jingchao Ni, Lu-An Tang, Jiaping Gui, Zhichun Li, Haifeng Chen, and Philip S. Yu. 2019. Heterogeneous Graph Matching Networks for Unknown Malware Detection. In Proc. International Joint Conference on Artificial Intelligence, (IJCAI). 3762\u20133770."},{"key":"e_1_2_1_58_1","volume-title":"Efficient Formal Safety Analysis of Neural Networks. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang , Kexin Pei , Justin Whitehouse , Junfeng Yang , and Suman Jana . 2018 . 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. 6369\u20136379. http:\/\/papers.nips.cc\/paper\/7873-efficient-formal-safety-analysis-of-neural-networks Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. 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. 6369\u20136379. http:\/\/papers.nips.cc\/paper\/7873-efficient-formal-safety-analysis-of-neural-networks"},{"key":"e_1_2_1_59_1","volume-title":"27th USENIX Security Symposium, USENIX Security 2018","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang , Kexin Pei , Justin Whitehouse , Junfeng Yang , and Suman Jana . 2018 . Formal Security Analysis of Neural Networks using Symbolic Intervals . In 27th USENIX Security Symposium, USENIX Security 2018 , Baltimore, MD, USA , August 15-17, 2018. 1599\u20131614. https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal Security Analysis of Neural Networks using Symbolic Intervals. In 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018. 1599\u20131614. https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi"},{"key":"e_1_2_1_60_1","volume-title":"Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624.","author":"Wang Shiqi","year":"2021","unstructured":"Shiqi Wang , Huan Zhang , Kaidi Xu , Xue Lin , Suman Jana , Cho-Jui Hsieh , and J Zico Kolter . 2021 . Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624. Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624."},{"key":"e_1_2_1_61_1","volume-title":"International Conference on Machine Learning. 5276\u20135285","author":"Weng Lily","year":"2018","unstructured":"Lily Weng , Huan Zhang , Hongge Chen , Zhao Song , Cho-Jui Hsieh , Luca Daniel , Duane Boning , and Inderjit Dhillon . 2018 . Towards fast computation of certified robustness for relu networks . In International Conference on Machine Learning. 5276\u20135285 . Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. 2018. Towards fast computation of certified robustness for relu networks. In International Conference on Machine Learning. 5276\u20135285."},{"key":"e_1_2_1_62_1","volume-title":"International Conference on Machine Learning. 5286\u20135295","author":"Wong Eric","year":"2018","unstructured":"Eric Wong and Zico Kolter . 2018 . Provable defenses against adversarial examples via the convex outer adversarial polytope . In International Conference on Machine Learning. 5286\u20135295 . Eric Wong and Zico Kolter. 2018. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning. 5286\u20135295."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7080246"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_20"},{"key":"e_1_2_1_65_1","volume-title":"Efficient Neural Network Analysis with Sum-of-Infeasibilities. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 143\u2013163","author":"Wu Haoze","year":"2022","unstructured":"Haoze Wu , Aleksandar Zelji\u0107 , Guy Katz , and Clark Barrett . 2022 . Efficient Neural Network Analysis with Sum-of-Infeasibilities. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 143\u2013163 . Haoze Wu, Aleksandar Zelji\u0107, Guy Katz, and Clark Barrett. 2022. Efficient Neural Network Analysis with Sum-of-Infeasibilities. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 143\u2013163."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNNLS.2020.2978386"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNNLS.2018.2808470"},{"key":"e_1_2_1_68_1","unstructured":"Kaidi Xu Huan Zhang Shiqi Wang Yihan Wang Suman Jana Xue Lin and Cho-Jui Hsieh. 2020. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. arXiv preprint arXiv:2011.13824. \t\t\t\t  Kaidi Xu Huan Zhang Shiqi Wang Yihan Wang Suman Jana Xue Lin and Cho-Jui Hsieh. 2020. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. arXiv preprint arXiv:2011.13824."},{"key":"e_1_2_1_69_1","first-page":"389","article-title":"Improving neural network verification through spurious region guided refinement","volume":"12651","author":"Yang Pengfei","year":"2021","unstructured":"Pengfei Yang , Renjue Li , Jianlin Li , Cheng-Chao Huang , Jingyi Wang , Jun Sun , Bai Xue , and Lijun Zhang . 2021 . Improving neural network verification through spurious region guided refinement . Tools and Algorithms for the Construction and Analysis of Systems , 12651 (2021), 389 . Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, and Lijun Zhang. 2021. Improving neural network verification through spurious region guided refinement. Tools and Algorithms for the Construction and Analysis of Systems, 12651 (2021), 389.","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3219819.3219890"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755913.1755940"},{"key":"e_1_2_1_72_1","unstructured":"Tom Zelazny Haoze Wu Clark Barrett and Guy Katz. 2022. On Optimizing Back-Substitution Methods for Neural Network Verification. arXiv preprint arXiv:2208.07669. \t\t\t\t  Tom Zelazny Haoze Wu Clark Barrett and Guy Katz. 2022. On Optimizing Back-Substitution Methods for Neural Network Verification. arXiv preprint arXiv:2208.07669."},{"key":"e_1_2_1_73_1","volume-title":"Advances in Neural Information Processing Systems","author":"Zhang Huan","year":"2018","unstructured":"Huan Zhang , Tsui-Wei Weng , Pin-Yu Chen , Cho-Jui Hsieh , and Luca Daniel . 2018. Efficient Neural Network Robustness Certification with General Activation Functions . In Advances in Neural Information Processing Systems , S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.). 31, Curran Associates, Inc. . https:\/\/proceedings.neurips.cc\/paper\/ 2018 \/file\/d04863f100d59b3eb688a11f95b0ae60-Paper.pdf Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient Neural Network Robustness Certification with General Activation Functions. In Advances in Neural Information Processing Systems, S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.). 31, Curran Associates, Inc.. https:\/\/proceedings.neurips.cc\/paper\/2018\/file\/d04863f100d59b3eb688a11f95b0ae60-Paper.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563325","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563325","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":73,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563325"],"URL":"https:\/\/doi.org\/10.1145\/3563325","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}