{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T11:41:20Z","timestamp":1780054880353,"version":"3.54.0"},"publisher-location":"New York, NY, USA","reference-count":88,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,11,6]],"date-time":"2019-11-06T00:00:00Z","timestamp":1572998400000},"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":[[2019,11,6]]},"DOI":"10.1145\/3319535.3354245","type":"proceedings-article","created":{"date-parts":[[2019,11,7]],"date-time":"2019-11-07T13:08:32Z","timestamp":1573132112000},"page":"1249-1264","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":69,"title":["Quantitative Verification of Neural Networks and Its Security Applications"],"prefix":"10.1145","author":[{"given":"Teodora","family":"Baluta","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shiqi","family":"Shen","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shweta","family":"Shinde","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Prateek","family":"Saxena","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,11,6]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"SAT'11","author":"Ab'io Ignasi","year":"2011"},{"key":"e_1_3_2_2_2_1","volume-title":"CP'13","author":"Ab'io Ignasi","year":"2013"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133904"},{"key":"e_1_3_2_2_4_1","volume-title":"Cardinality networks: a theoretical and empirical study. Constraints","author":"As'in Roberto","year":"2011"},{"key":"e_1_3_2_2_5_1","volume-title":"ICML'18","author":"Athalye Anish","year":"2018"},{"key":"e_1_3_2_2_6_1","volume-title":"ICLR'15","author":"Bahdanau Dzmitry","year":"2015"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1468075.1468121"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICUAS.2015.7152300"},{"key":"e_1_3_2_2_9_1","volume-title":"Davide Del Testa","author":"Bojarski Mariusz","year":"2016"},{"key":"e_1_3_2_2_10_1","volume-title":"The Secret Sharer: Measuring Unintended Neural Network Memorization & Extracting Secrets. arXiv","author":"Carlini Nicholas","year":"2018"},{"key":"e_1_3_2_2_11_1","volume-title":"Towards Evaluating the Robustness of Neural Networks. In SP'17","author":"Carlini Nicholas","year":"2017"},{"key":"e_1_3_2_2_12_1","volume-title":"AAAI'14","author":"Chakraborty Supratik","year":"2014"},{"key":"e_1_3_2_2_13_1","volume-title":"IJCAI'15","author":"Chakraborty Supratik","year":"2015"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593097"},{"key":"e_1_3_2_2_16_1","volume-title":"IJCAI'16","author":"Chakraborty Supratik","year":"2016"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134097"},{"key":"e_1_3_2_2_18_1","volume-title":"Limitations of adversarial robustness: strong No Free Lunch Theorem. arXiv","author":"Dohmatob Elvis","year":"2018"},{"key":"e_1_3_2_2_19_1","volume-title":"IJCAI'16","author":"Dudek Jeffrey M."},{"key":"e_1_3_2_2_20_1","volume-title":"The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas. In IJCAI'17","author":"Dudek Jeffrey M."},{"key":"e_1_3_2_2_21_1","volume-title":"UAI'18","author":"Dvijotham Krishnamurthy","year":"2018"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2090236.2090255"},{"key":"e_1_3_2_2_23_1","first-page":"1","article-title":"Translating Pseudo-Boolean Constraints into SAT","volume":"2","author":"E\u00e9n Niklas","year":"2006","journal-title":"JSAT"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_2_2_25_1","volume-title":"ICML'13","author":"Ermon Stefano","year":"2013"},{"key":"e_1_3_2_2_26_1","volume-title":"CVPR'18","author":"Evtimov Ivan","year":"2018"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2783258.2783311"},{"key":"e_1_3_2_2_28_1","volume-title":"ICML'19","author":"Ford Nic","year":"2019"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813677"},{"key":"e_1_3_2_2_30_1","volume-title":"Attacking Binarized Neural Networks. In ICLR'18","author":"Galloway Angus","year":"2018"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359789.3359790"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_2_2_33_1","volume-title":"Motivating the rules of the game for adversarial example research. arXiv","author":"Gilmer Justin","year":"2018"},{"key":"e_1_3_2_2_34_1","volume-title":"Adversarial spheres. arXiv","author":"Gilmer Justin","year":"2018"},{"key":"e_1_3_2_2_35_1","volume-title":"Davide Scaramuzza, and Luca M. Gambardella.","author":"Giusti Alessandro","year":"2016"},{"key":"e_1_3_2_2_36_1","volume-title":"AAAI'06","author":"Gomes Carla P.","year":"2006"},{"key":"e_1_3_2_2_37_1","volume-title":"Explaining and Harnessing Adversarial Examples. In ICLR'15","author":"Goodfellow Ian","year":"2015"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_18"},{"key":"e_1_3_2_2_39_1","volume-title":"NIPS'16","author":"Hardt Moritz","year":"2016"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"crossref","unstructured":"W Keith Hastings. 1970. Monte Carlo sampling methods using Markov chains and their applications. (1970).  W Keith Hastings. 1970. Monte Carlo sampling methods using Markov chains and their applications. (1970).","DOI":"10.1093\/biomet\/57.1.97"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.90"},{"key":"e_1_3_2_2_42_1","volume-title":"Sound Abstraction and Decomposition of Probabilistic Programs. In ICML'18","author":"Holtzen Steven","year":"2018"},{"key":"e_1_3_2_2_43_1","volume-title":"Safety Verification of Deep Neural Networks. In CAV'17","author":"Huang Xiaowei","year":"2017"},{"key":"e_1_3_2_2_44_1","volume-title":"NIPS'16","author":"Hubara Itay","year":"2016"},{"key":"e_1_3_2_2_45_1","volume-title":"Jerrum and Alistair Sinclair","author":"Mark","year":"1996"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2016.7778091"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_2_48_1","volume-title":"NIPS'12","author":"Krizhevsky Alex","year":"2012"},{"key":"e_1_3_2_2_49_1","volume-title":"Efficient object detection using embedded binarized neural networks. Journal of Signal Processing Systems","author":"Kung Jaeha","year":"2018"},{"key":"e_1_3_2_2_50_1","unstructured":"Yann LeCun and Corinna Cortes. 2010. MNIST handwritten digit database. (2010).  Yann LeCun and Corinna Cortes. 2010. MNIST handwritten digit database. (2010)."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2018.00191"},{"key":"e_1_3_2_2_52_1","volume-title":"Trojaning Attack on Neural Networks. In NDSS'18","author":"Liu Yingqi","year":"2018"},{"key":"e_1_3_2_2_53_1","volume-title":"The curse of concentration in robust learning: Evasion and poisoning attacks from concentration of measure. arXiv","author":"Mahloujifar Saeed","year":"2018"},{"key":"e_1_3_2_2_54_1","volume-title":"Embedded Binarized Neural Networks. In EWSN'17","author":"McDanel Bradley","year":"2017"},{"key":"e_1_3_2_2_56_1","volume-title":"Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh.","author":"Narodytska Nina","year":"2018"},{"key":"e_1_3_2_2_57_1","volume-title":"Assessing Heuristic Machine Learning Explanations with Model Counting. In SAT'19","author":"Narodytska Nina","year":"2019"},{"key":"e_1_3_2_2_58_1","unstructured":"Radford M Neal. 1993. Probabilistic inference using Markov chain Monte Carlo methods. (1993).  Radford M Neal. 1993. Probabilistic inference using Markov chain Monte Carlo methods. (1993)."},{"key":"e_1_3_2_2_59_1","volume-title":"Transferability in Machine Learning: from Phenomena to Black-Box Attacks using Adversarial Samples. arXiv","author":"Papernot Nicolas","year":"2016"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"crossref","unstructured":"Nicolas Papernot Patrick McDaniel Somesh Jha Matt Fredrikson Z Berkay Celik and Ananthram Swami. 2016b. The limitations of deep learning in adversarial settings. In EuroS&P'16.  Nicolas Papernot Patrick McDaniel Somesh Jha Matt Fredrikson Z Berkay Celik and Ananthram Swami. 2016b. The limitations of deep learning in adversarial settings. In EuroS&P'16.","DOI":"10.1109\/EuroSP.2016.36"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.41"},{"key":"e_1_3_2_2_62_1","unstructured":"Adam Paszke Sam Gross Soumith Chintala Gregory Chanan Edward Yang Zachary DeVito Zeming Lin Alban Desmaison Luca Antiga and Adam Lerer. 2017. Automatic differentiation in PyTorch. In NIPS-W'17.  Adam Paszke Sam Gross Soumith Chintala Gregory Chanan Edward Yang Zachary DeVito Zeming Lin Alban Desmaison Luca Antiga and Adam Lerer. 2017. Automatic differentiation in PyTorch. In NIPS-W'17."},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132785"},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_2"},{"key":"e_1_3_2_2_65_1","volume-title":"Phase Transition Behavior of Cardinality and XOR Constraints. In International Joint Conferences on Artificial Intelligence.","author":"Pote Yash","year":"2019"},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"e_1_3_2_2_67_1","volume-title":"ICLR'18","author":"Raghunathan Aditi","year":"2018"},{"key":"e_1_3_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46493-0_32"},{"key":"e_1_3_2_2_69_1","volume-title":"Reachability Analysis of Deep Neural Networks with Provable Guarantees. In IJCAI'18","author":"Ruan Wenjie","year":"2018"},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_25"},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.41"},{"key":"e_1_3_2_2_72_1","volume-title":"NIPS'18","author":"Singh Gagandeep","year":"2018"},{"key":"e_1_3_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_73"},{"key":"e_1_3_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011592"},{"key":"e_1_3_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808740"},{"key":"e_1_3_2_2_77_1","volume-title":"NIPS'14","author":"Sutskever Ilya","year":"2014"},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2015.7298594"},{"key":"e_1_3_2_2_79_1","volume-title":"ICLR'14","author":"Szegedy Christian","year":"2014"},{"key":"e_1_3_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1989.63527"},{"key":"e_1_3_2_2_81_1","volume-title":"ICLR'18","author":"Tram\u00e8r Florian","year":"2018"},{"key":"e_1_3_2_2_82_1","doi-asserted-by":"crossref","unstructured":"Grigori S Tseitin. 1983. On the complexity of derivation in propositional calculus. In Automation of reasoning.  Grigori S Tseitin. 1983. On the complexity of derivation in propositional calculus. In Automation of reasoning.","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_3_2_2_83_1","volume-title":"ICML'18","author":"Uesato Jonathan"},{"key":"e_1_3_2_2_84_1","series-title":"SIAM J. Comput. (1979)","volume-title":"The complexity of enumeration and reliability problems","author":"Valiant Leslie G."},{"key":"e_1_3_2_2_85_1","volume-title":"AtomNet: A deep convolutional neural network for bioactivity prediction in structure-based drug discovery. arXiv","author":"Wallach Izhar","year":"2015"},{"key":"e_1_3_2_2_86_1","volume-title":"USENIX'18","author":"Wang Shiqi","year":"2018"},{"key":"e_1_3_2_2_87_1","volume-title":"ICLR'19","author":"Webb Stefan","year":"2019"},{"key":"e_1_3_2_2_88_1","volume-title":"ICML'18","author":"Wong Eric","year":"2018"},{"key":"e_1_3_2_2_89_1","volume-title":"AISTATS'15","author":"Zafar Muhammad Bilal","year":"2015"}],"event":{"name":"CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security","location":"London United Kingdom","acronym":"CCS '19","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319535.3354245","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3319535.3354245","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:24:03Z","timestamp":1750202643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319535.3354245"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,6]]},"references-count":88,"alternative-id":["10.1145\/3319535.3354245","10.1145\/3319535"],"URL":"https:\/\/doi.org\/10.1145\/3319535.3354245","relation":{},"subject":[],"published":{"date-parts":[[2019,11,6]]},"assertion":[{"value":"2019-11-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}