{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T17:59:38Z","timestamp":1775066378110,"version":"3.50.1"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T00:00:00Z","timestamp":1720742400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1900676, 2019239, 2129824, 2200621, 2217071, 2238133, 231913"],"award-info":[{"award-number":["1900676, 2019239, 2129824, 2200621, 2217071, 2238133, 231913"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2024,7,12]]},"abstract":"<jats:p>Deep Neural Networks (DNN) have emerged as an effective approach to tackling real-world problems. However, like human-written software, DNNs are susceptible to bugs and attacks. This has generated significant interest in developing effective and scalable DNN verification techniques and tools.<\/jats:p>\n                  <jats:p>Recent developments in DNN verification have highlighted the potential of constraint-solving approaches that combine abstraction techniques with SAT solving. Abstraction approaches are effective at precisely encoding neuron behavior when it is linear, but they lead to overapproximation and combinatorial scaling when behavior is non-linear. SAT approaches in DNN verification have incorporated standard DPLL techniques, but have overlooked important optimizations found in modern SAT solvers that help them scale on industrial benchmarks.<\/jats:p>\n                  <jats:p>\n                    In this paper, we present\n                    <jats:monospace>VeriStable<\/jats:monospace>\n                    , a novel extension of the recently proposed DPLL-based constraint DNN verification approach.\n                    <jats:monospace>VeriStable<\/jats:monospace>\n                    leverages the insight that while neuron behavior may be non-linear across the entire DNN input space, at intermediate states computed during verification many neurons may be constrained to have linear behavior - these neurons are stable. Efficiently detecting stable neurons reduces combinatorial complexity without compromising the precision of abstractions. Moreover, the structure of clauses arising in DNN verification problems shares important characteristics with industrial SAT benchmarks. We adapt and incorporate multi-threading and restart optimizations targeting those characteristics to further optimize DPLL-based DNN verification.\n                  <\/jats:p>\n                  <jats:p>\n                    We evaluate the effectiveness of\n                    <jats:monospace>VeriStable<\/jats:monospace>\n                    across a range of challenging benchmarks including fullyconnected feedforward networks (FNNs), convolutional neural networks (CNNs) and residual networks (ResNets) applied to the standard MNIST and CIFAR datasets. Preliminary results show that\n                    <jats:monospace>VeriStable<\/jats:monospace>\n                    is competitive and outperforms state-of-the-art DNN verification tools, including\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>\u03b1<\/mml:mi>\n                        <mml:mo>\u2212<\/mml:mo>\n                        <mml:mi>\u03b2<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    -\n                    <jats:monospace>CROWN<\/jats:monospace>\n                    and\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mtext>MN<\/mml:mtext>\n                        <mml:mo>\u2212<\/mml:mo>\n                        <mml:mtext>BaB<\/mml:mtext>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    , the first and second performers of the VNN-COMP, respectively.\n                  <\/jats:p>","DOI":"10.1145\/3643765","type":"journal-article","created":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T10:22:09Z","timestamp":1720779729000},"page":"859-881","source":"Crossref","is-referenced-by-count":12,"title":["Harnessing Neuron Stability to Improve DNN Verification"],"prefix":"10.1145","volume":"1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3341-9794","authenticated-orcid":false,"given":"Hai","family":"Duong","sequence":"first","affiliation":[{"name":"George Mason University, Fairfax, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5643-7197","authenticated-orcid":false,"given":"Dong","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Virginia, Charlottesville, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4255-4592","authenticated-orcid":false,"given":"Thanhvu","family":"Nguyen","sequence":"additional","affiliation":[{"name":"George Mason University, Fairfax, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1937-1544","authenticated-orcid":false,"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[{"name":"University of Virginia, Charlottesville, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,7,12]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_2"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_2"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Stanley Bak Changliu Liu and Taylor Johnson . 2021. The Second International verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. (2021). https:\/\/doi.org\/10.48550\/arXiv.2109.00498 10.48550\/arXiv.2109.00498","DOI":"10.48550\/arXiv.2109.00498"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190039"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1550723"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-16437-8_73"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2301.05815"},{"issue":"2020","key":"e_1_3_1_13_1","first-page":"3455716.3455758","article-title":"Branch and bound for piecewise linear neural network verification","volume":"21","author":"Bunel Rudy","year":"2020","unstructured":"Rudy Bunel , P Mudigonda , Ilker Turkaslan , P Torr , Jingyue Lu , and Pushmeet Kohli . 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research 21, 2020 (2020). 3455716.3455758","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_1_14_1","unstructured":"Tianlong Chen Huan Zhang Zhenyu Zhang Shiyu Chang Sijia Liu Pin-Yu Chen and Zhangyang Wang . 2022. Linearity grafting: Relaxed neuron pruning helps certifiable robustness. In International Conference on Machine Learning. PMLR 3760-3772. https:\/\/proceedings.mlr.press\/v162\/chen22af\/chen22af.pdf"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2104.06718"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576040"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2307.10266"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ymssp.2021.108153"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2887965.2887988"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2205.00263"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"Chuqin Geng Nham Le Xiaojie Xu Zhaoyue Wang Arie Gurfinkel and Xujie Si . 2023. Towards reliable neural specifications. In International Conference on Machine Learning. PMLR 11196-11212. https:\/\/dl.acm.org\/doi\/10.5555\/3618408.3618857 10.5555\/3618408.3618857","DOI":"10.5555\/3618408.3618857"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/3070217.3070238"},{"key":"e_1_3_1_29_1","first-page":"315","article-title":"Deep sparse rectifier neural networks","author":"Glorot Xavier","year":"2011","unstructured":"Xavier Glorot , Antoine Bordes , and Yoshua Bengio . 2011. Deep sparse rectifier neural networks. In Proceedings of the fourteenth international conference on artificial intelligence and statistics. JMLR Workshop and Conference Proceedings, 315-323. https:\/\/proceedings.mlr.press\/v15\/glorot11a\/glorot11a.pdf","journal-title":"In Proceedings of the fourteenth international conference on artificial intelligence and statistics. JMLR Workshop and Conference Proceedings"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/295240.295710"},{"key":"e_1_3_1_31_1","article-title":"Deep learning","author":"Goodfellow Ian","year":"2016","unstructured":"Ian Goodfellow , Yoshua Bengio , and Aaron Courville . 2016. Deep learning. MIT press. https:\/\/mitpress.mit.edu\/9780262035613\/deep-learning\/","journal-title":"MIT press."},{"key":"e_1_3_1_32_1","unstructured":"Gurobi Optimization LLC. 2022. Gurobi Optimizer Reference Manual. https:\/\/www.gurobi.com"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCV.2015.123"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.90"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA200385"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00363-7"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Jinhan Kim Robert Feldt and Shin Yoo . 2019. Guiding deep learning system testing using surprise adequacy. In 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE). IEEE 1039-1049. https:\/\/doi.org\/10.1109\/ICSE.2019.00108 10.1109\/ICSE.2019.00108","DOI":"10.1109\/ICSE.2019.00108"},{"key":"e_1_3_1_41_1","volume-title":"Technical Report","author":"Kochenderfer Mykel J","year":"2012","unstructured":"Mykel J Kochenderfer , Jessica E Holland , and James P Chryssanthacopoulos . 2012. Next-generation airborne collision avoidance system. Technical Report. Massachusetts Institute of Technology-Lincoln Laboratory Lexington United States. https:\/\/www.ll.mit.edu\/sites\/default\/files\/page\/doc\/2018-05\/19_1_1_Kochenderfer.pdf"},{"key":"e_1_3_1_42_1","article-title":"Decision procedures","author":"Kroening Daniel","year":"2008","unstructured":"Daniel Kroening and Ofer Strichman . 2008. Decision procedures. Springer. https:\/\/dl.acm.org\/doi\/10.5555\/1391237","journal-title":"Springer."},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Ludovic Le Frioux Souheib Baarir Julien Sopena and Fabrice Kordon . 2017. PaInleSS: A Framework for Parallel SAT Solving. In Theory and Applications of Satisfiability Testing-SAT 2017: 20th International Conference Melbourne VIC Australia August 28-September 1 2017 Proceedings 20. Springer 233-250. https:\/\/doi.org\/10.1007\/978-3-319-66263-3_15 10.1007\/978-3-319-66263-3_15","DOI":"10.1007\/978-3-319-66263-3_15"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_8"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11760-022-02222-2"},{"key":"e_1_3_1_46_1","first-page":"3","volume-title":"Proc. icml","author":"Maas Andrew L","year":"2013","unstructured":"Andrew L Maas , Awni Y Hannun , Andrew Y Ng , et al. 2013. Rectifier nonlinearities improve neural network acoustic models. In Proc. icml, Vol. 30. Atlanta, GA, 3. https:\/\/ai.stanford.edu\/~amaas\/papers\/relu_hybrid_icml2013_final.pdf"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1177\/00031348221101490"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2007.10868"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2212.10376"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_1_51_1","unstructured":"OVAL-group. 2023. OVAL-Branch-and-Bound-based Neural Network Verification. https:\/\/github.com\/oval-group\/oval-bab."},{"key":"e_1_3_1_52_1","first-page":"726","article-title":"Safety-enhanced autonomous driving using interpretable sensor fusion transformer","author":"Shao Hao","year":"2023","unstructured":"Hao Shao , Letian Wang , Ruobing Chen , Hongsheng Li , and Yu Liu . 2023. Safety-enhanced autonomous driving using interpretable sensor fusion transformer. In Conference on Robot Learning. PMLR, 726-737. https:\/\/proceedings.mlr.press\/v205\/shao23a\/shao23a.pdf","journal-title":"In Conference on Robot Learning. PMLR"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_6"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","unstructured":"David Shriver Sebastian Elbaum and Matthew B Dwyer. 2021. Reducing DNN Properties to Enable Falsification with Adversarial Attacks. In 2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE). IEEE 275-287. https:\/\/doi.org\/10.1109\/ICSE43902.2021.00036 10.1109\/ICSE43902.2021.00036","DOI":"10.1109\/ICSE43902.2021.00036"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/3454287.3455639"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/3327546.3327739"},{"key":"e_1_3_1_57_1","article-title":"Boosting robustness certification of neural networks","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh , Timon Gehr , Markus P\u00fcschel , and Martin Vechev . 2018b. Boosting robustness certification of neural networks. In International Conference on Learning Representations. https:\/\/files.sri.inf.ethz.ch\/website\/papers\/RefineZono.pdf","journal-title":"In International Conference on Learning Representations."},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3358233"},{"key":"e_1_3_1_60_1","unstructured":"Armando Tacchella Luca Pulina Dario Guidotti and Stefano Demarchi . 2023. The international benchmarks standard for the Verification of Neural Networks. https:\/\/www.vnnlib.org\/"},{"key":"e_1_3_1_61_1","article-title":"Evaluating Robustness of Neural Networks with Mixed Integer Programming","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 International Conference on Learning Representations. https:\/\/doi.org\/1721.1\/119563 1721.1\/119563","journal-title":"In International Conference on Learning Representations"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3613079"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_12"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/3327345.3327533"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/3277203.3277323"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2103.06624"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_20"},{"key":"e_1_3_1_69_1","unstructured":"Kai Yuanqing Xiao Vincent Tjeng Nur Muhammad (Mahi) Shafiullah and Aleksander Madry . 2019. Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability. In 7th International Conference on Learning Representations ICLR 2019 New Orleans LA USA May 6-9 2019. https:\/\/doi.org\/1721.1\/130110 1721.1\/130110"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_2"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_5"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/3495724.3495820"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2011.13824"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219455423501316"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1906.06316"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/3600270.3600391"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","DOI":"10.5555\/3327345.3327402"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2001.968634"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253717"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","unstructured":"LI Zhangheng Tianlong Chen Linyi Li Bo Li and Zhangyang Wang . 2022. Can Pruning Improve Certified Robustness of Neural Networks? Transactions on Machine Learning Research (2022). https:\/\/doi.org\/10.48550\/arXiv.2206.07311 10.48550\/arXiv.2206.07311","DOI":"10.48550\/arXiv.2206.07311"},{"key":"e_1_3_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464811"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643765","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3643765","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3643765","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:57:19Z","timestamp":1770191839000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643765"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,12]]},"references-count":80,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2024,7,12]]}},"alternative-id":["10.1145\/3643765"],"URL":"https:\/\/doi.org\/10.1145\/3643765","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,12]]}}}