{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T02:37:16Z","timestamp":1777775836511,"version":"3.51.4"},"reference-count":294,"publisher":"Emerald","issue":"3-4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>Deep neural networks (DNNs) now dominate the AI landscape and have shown impressive performance in diverse application domains, including vision, natural language processing (NLP), and healthcare. However, both public and private entities have been increasingly expressing significant concern about the potential of state-of-the-art AI models to cause societal and financial harm. This lack of trust arises from their black-box construction and vulnerability against natural and adversarial noise.<\/jats:p>\n                  <jats:p>As a result, researchers have spent considerable time developing automated methods for building safe and trustworthy DNNs. Abstract interpretation has emerged as the most popular framework for efficiently analyzing realistic DNNs among the various approaches. However, due to fundamental differences in the computational structure (e.g., high nonlinearity) of DNNs compared to traditional programs, developing efficient DNN analyzers has required tackling significantly different research challenges than encountered for programs.<\/jats:p>\n                  <jats:p>In this monograph, we describe state-of-the-art approaches based on abstract interpretation for analyzing DNNs. These approaches include the design of new abstract domains, synthesis of novel abstract transformers, abstraction refinement, and incremental analysis. We will discuss how the analysis results can be used to: (i) formally check whether a trained DNN satisfies desired output and gradient-based safety properties, (ii) guide the model updates during training towards satisfying safety properties, and (iii) reliably explain and interpret the black-box workings of DNNs.<\/jats:p>","DOI":"10.1561\/2500000062","type":"journal-article","created":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T08:02:38Z","timestamp":1750924958000},"page":"250-408","source":"Crossref","is-referenced-by-count":3,"title":["Safety and Trust in Artificial Intelligence with Abstract Interpretation"],"prefix":"10.1108","volume":"8","author":[{"given":"Gagandeep","family":"Singh","sequence":"first","affiliation":[{"name":"University of Illinois Urbana-Champaign ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob","family":"Laurel","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sasa","family":"Misailovic","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Debangshu","family":"Banerjee","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avaljot","family":"Singh","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Changming","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shubham","family":"Ugare","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huan","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"140","published-online":{"date-parts":[[2025,6,30]]},"reference":[{"key":"2026032910310568300_ref001","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-540-69166-2_13","volume-title":"Static Analysis","author":"Allamigeon","year":"2008"},{"key":"2026032910310568300_ref002","article-title":"Towards robust inter-pretability with self-explaining neural networks","volume-title":"Neural Information Processing Systems","author":"Alvarez-Melis","year":"2018"},{"issue":"2","key":"2026032910310568300_ref003","doi-asserted-by":"crossref","DOI":"10.2478\/v10136-012-0031-x","article-title":"Artificial neural networks in medical diagnosis","volume":"11","author":"Amato","year":"2013","journal-title":"Journal of Applied Biomedicine"},{"key":"2026032910310568300_ref004","first-page":"731","article-title":"Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness","volume-title":"Proc. Programming Language Design and Implementation (PLDI)","author":"Anderson","year":"2019"},{"issue":"1","key":"2026032910310568300_ref005","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10107-020-01474-5","article-title":"Strong mixed-integer programming formulations for trained neural networks","volume":"183","author":"Anderson","year":"2020","journal-title":"Mathematical Programming"},{"key":"2026032910310568300_ref006","first-page":"291","article-title":"Sorting Out Lipschitz Function Approximation","author":"Anil","year":"2019"},{"key":"2026032910310568300_ref007","article-title":"Universal Approximation with Certified Networks","author":"Baader","year":"2020"},{"key":"2026032910310568300_ref008","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-030-76384-8_2","article-title":"nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement","author":"Bak","year":"2021"},{"key":"2026032910310568300_ref009","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-031-27481-7_26","article-title":"The Octatope Abstract Domain for Verification of Neural Networks","author":"Bak","year":"2023"},{"issue":"1","key":"2026032910310568300_ref010","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-024-00457-y","article-title":"The hexatope and octatope abstract domains for neural network verification","volume":"64","author":"Bak","year":"2024","journal-title":"Form. Methods Syst. Des."},{"key":"2026032910310568300_ref011","article-title":"The second international verification of neural networks competition (vnn-comp 2021): Summary and results","volume-title":"arXiv preprint","author":"Bak","year":"2021"},{"key":"2026032910310568300_ref012","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-030-53288-8_4","article-title":"Improved Geometric Path Enumeration for Verifying ReLU Neural Networks","author":"Bak","year":"2020"},{"key":"2026032910310568300_ref013","volume-title":"Advances in Neural Information Processing Systems","author":"Balunovic","year":"2019"},{"key":"2026032910310568300_ref014","article-title":"Adversarial Training and Provable Defenses: Bridging the Gap","author":"Balunovic","year":"2020"},{"key":"2026032910310568300_ref015","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1109\/ICSE43902.2021.00039","article-title":"Scalable Quantitative Verification For Deep Neural Networks","author":"Baluta","year":"2021"},{"key":"2026032910310568300_ref016","article-title":"Interpreting Robustness Proofs of Deep Neural Networks","author":"Banerjee","year":"2024"},{"key":"2026032910310568300_ref017","article-title":"Relational DNN Verification With Cross Executional Bound Refinement","author":"Banerjee","year":"2024"},{"issue":"PLDI","key":"2026032910310568300_ref018","doi-asserted-by":"publisher","DOI":"10.1145\/3656377","article-title":"Input-Relational Verification of Deep Neural Networks","volume":"8","author":"Banerjee","year":"2024","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref019","first-page":"3663","article-title":"Certifi-ably robust variational autoencoders","author":"Barrett","year":"2022"},{"key":"2026032910310568300_ref020","first-page":"4906","article-title":"Tight Verification of Probabilistic Robustness in Bayesian Neural Networks","author":"Batten","year":"2024"},{"key":"2026032910310568300_ref021","volume-title":"Adult","author":"Becker","year":"1996"},{"key":"2026032910310568300_ref022","first-page":"610","article-title":"On the Dangers of Stochastic Parrots: Can Language Models Be Too Big?","author":"Bender","year":"2021"},{"key":"2026032910310568300_ref023","volume-title":"FADBAD, a flexible C++ package for automatic differentiation","author":"Bendtsen","year":"1996"},{"key":"2026032910310568300_ref024","first-page":"11136","article-title":"Make Sure You\u2019re Unsure: A Framework for Verifying Probabilistic Specifications","author":"Berrada","year":"2021"},{"key":"2026032910310568300_ref025","article-title":"What is the State of Neural Network Pruning?","author":"Blalock","year":"2020"},{"key":"2026032910310568300_ref026","first-page":"5230","article-title":"Efficient and modular implicit differentiation","volume":"35","author":"Blondel","year":"2022","journal-title":"Advances in neural information processing systems"},{"key":"2026032910310568300_ref027","article-title":"End to end learning for self-driving cars","volume-title":"arXiv preprint","author":"Bojarski","year":"2016"},{"key":"2026032910310568300_ref028","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1145\/3453483.3454056","article-title":"Fast and precise certification of transformers","author":"Bonaert","year":"2021"},{"key":"2026032910310568300_ref029","first-page":"3240","article-title":"Cnn-cert: An efficient framework for certifying robustness of convo-lutional neural networks","author":"Boopathy","year":"2019"},{"issue":"2-4","key":"2026032910310568300_ref030","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/S00607-011-0182-8","article-title":"A generalization of p-boxes to affine arithmetic","volume":"94","author":"Bouissou","year":"2012","journal-title":"Computing"},{"key":"2026032910310568300_ref031","first-page":"225","article-title":"Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities","author":"Bouissou","year":"2016"},{"key":"2026032910310568300_ref032","article-title":"The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results","volume-title":"arXiv preprint","author":"Brix","year":"2024"},{"key":"2026032910310568300_ref033","unstructured":"Brix, C., S.Bak, T. T.Johnson, and H.Wu. (2024b). \u201cThe Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results\u201d. URL: https:\/\/arxiv.org\/abs\/2412.19985."},{"key":"2026032910310568300_ref034","article-title":"The fourth international verification of neural networks competition (VNN-COMP 2023): Summary and results","volume-title":"arXiv preprint","author":"Brix","year":"2023"},{"key":"2026032910310568300_ref035","article-title":"Language Models are Few-Shot Learners","volume-title":"Proc. Advances in Neural Information Processing Systems (NeurIPS)","author":"Brown","year":"2020"},{"key":"2026032910310568300_ref036","unstructured":"Br\u00fcckner, B. and A.Lomuscio. (2024). \u201cVerification of Neural Networks against Convolutional Perturbations via Parameterised Kernels\u201d. URL: https:\/\/arxiv.org\/abs\/2411.04594."},{"issue":"2020","key":"2026032910310568300_ref037","article-title":"Branch and bound for piecewise linear neural network verification","volume":"21","author":"Bunel","year":"2020","journal-title":"Journal of Machine Learning Research"},{"key":"2026032910310568300_ref038","first-page":"3565","article-title":"Towards a theoretical understanding of the robustness of variational autoencoders","author":"Camuto","year":"2021"},{"key":"2026032910310568300_ref039","article-title":"Property-Driven Evaluation of RL-Controllers in Self-Driving Datacenters","author":"Chakravarthy","year":"2022"},{"key":"2026032910310568300_ref040","first-page":"32","article-title":"Neural lyapunov control","volume-title":"Advances in Neural Information Processing Systems","author":"Chang","year":"2019"},{"key":"2026032910310568300_ref041","article-title":"Certifying Counterfactual Bias in LLMs","author":"Chaudhary","year":"2025"},{"key":"2026032910310568300_ref042","unstructured":"Chaudhary, I., V. V.Jain, and G.Singh. (2024a). \u201cDecoding Intelligence: A Framework for Certifying Knowledge Comprehension in LLMs\u201d. URL: https:\/\/arxiv.org\/abs\/2402.15929."},{"key":"2026032910310568300_ref043","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2412.03028","article-title":"Specification Generation for Neural Networks in Systems","volume":"abs\/2412.03028","author":"Chaudhary","year":"2024","journal-title":"CoRR"},{"key":"2026032910310568300_ref044","first-page":"477","article-title":"Learning Security Classifiers with Verified Global Robustness Properties","author":"Chen","year":"2021"},{"key":"2026032910310568300_ref045","article-title":"GPU-Accelerated Verification of Machine Learning Models for Power Systems","volume-title":"arXiv preprint","author":"Chevalier","year":"2023"},{"key":"2026032910310568300_ref046","unstructured":"Chevalier, S., D.Starkenburg, and K.Dvijotham. (2024). \u201cAchieving the Tightest Relaxation of Sigmoids for Formal Verification\u201d. URL: https:\/\/arxiv.org\/abs\/2408.10491."},{"key":"2026032910310568300_ref047","article-title":"Certified Defenses for Adversarial Patches","author":"Chiang","year":"2020"},{"key":"2026032910310568300_ref048","first-page":"1","article-title":"An Automated Approach to Accelerate DNNs on Edge Devices","author":"Chugh","year":"2021"},{"key":"2026032910310568300_ref049","unstructured":"Cohen, N., M.Ducoffe, R.Boumazouza, C.Gabreau, C.Pagetti, X.Pucel, and A.Galametz. (2024). \u201cVerification for Object Detection -IBP IoU\u201d. url: https:\/\/arxiv.org\/abs\/2403.08788."},{"key":"2026032910310568300_ref050","article-title":"Computing the range of derivatives","volume-title":"IMACS Annals on Computing and Applied Mathematics,(to appear)","author":"Corliss","year":"1991"},{"key":"2026032910310568300_ref051","volume-title":"Principles of abstract interpretation","author":"Cousot","year":"2021"},{"key":"2026032910310568300_ref052","first-page":"238","article-title":"Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints","author":"Cousot","year":"1977"},{"key":"2026032910310568300_ref053","doi-asserted-by":"crossref","DOI":"10.1145\/512760.512770","article-title":"Automatic Discovery of Linear Restraints Among Variables of a Program","author":"Cousot","year":"1978"},{"key":"2026032910310568300_ref054","first-page":"169","article-title":"Probabilistic abstract interpretation","author":"Cousot","year":"2012"},{"key":"2026032910310568300_ref055","doi-asserted-by":"publisher","first-page":"712","DOI":"10.3233\/FAIA200158","article-title":"On the Reasons Behind Decisions","author":"Darwiche","year":"2020"},{"key":"2026032910310568300_ref056","article-title":"Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming","author":"Dathathri","year":"2020"},{"key":"2026032910310568300_ref057","first-page":"47","article-title":"Supporting Standardization of Neural Networks Verification with VNNLIB and CoCoNet","volume-title":"FoMLAS@ CAV","author":"Demarchi","year":"2023"},{"key":"2026032910310568300_ref058","first-page":"248","article-title":"Imagenet: A large-scale hierarchical image database","author":"Deng","year":"2009"},{"key":"2026032910310568300_ref059","volume-title":"Global Derivatives","author":"Deussen","year":"2021"},{"key":"2026032910310568300_ref060","article-title":"Prov-ably Robust Adversarial Examples","author":"Dimitrov","year":"2022"},{"key":"2026032910310568300_ref061","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2307.10266","article-title":"A DPLL(T) Framework for Verifying Deep Neural Networks","volume":"abs\/2307.10266","author":"Duong","year":"2023","journal-title":"CoRR"},{"key":"2026032910310568300_ref062","unstructured":"Dvijotham, K., M.Garnelo, A.Fawzi, and P.Kohli. (2018a). \u201cVerification of deep probabilistic models\u201d. URL: https:\/\/arxiv.org\/abs\/1812.02795."},{"key":"2026032910310568300_ref063","first-page":"550","article-title":"A Dual Approach to Scalable Verification of Deep Networks","author":"Dvijotham","year":"2018"},{"key":"2026032910310568300_ref064","first-page":"214","article-title":"Fairness through awareness","author":"Dwork","year":"2012"},{"key":"2026032910310568300_ref065","doi-asserted-by":"crossref","DOI":"10.1007\/11681878_14","article-title":"Calibrating noise to sensitivity in private data analysis","volume-title":"Theory of cryptography conference","author":"Dwork","year":"2006"},{"key":"2026032910310568300_ref066","article-title":"Efficient Error Certification for Physics-Informed Neural Networks","author":"Eiras","year":"2023"},{"key":"2026032910310568300_ref067","article-title":"Adversarial Training and Provable Robustness: A Tale of Two Objectives","volume":"abs\/2008.06081","author":"Fan","year":"2020","journal-title":"CoRR"},{"key":"2026032910310568300_ref068","doi-asserted-by":"crossref","unstructured":"Fazlyab, M., M.Morari, and G. J.Pappas. (2019a). \u201cProbabilistic Verification and Reachability Analysis of Neural Networks via Semidefinite Programming\u201d. URL: https:\/\/arxiv.org\/abs\/1910.04249.","DOI":"10.1109\/CDC40024.2019.9029310"},{"key":"2026032910310568300_ref069","first-page":"32","article-title":"Efficient and accurate estimation of lipschitz constants for deep neural networks","volume-title":"Advances in neural information processing systems","author":"Fazlyab","year":"2019"},{"key":"2026032910310568300_ref070","article-title":"Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound","author":"Ferrari","year":"2022"},{"key":"2026032910310568300_ref071","unstructured":"Ferson, S., V.Kreinovich, L.Grinzburg, D.Myers, and K.Sentz. (2015). \u201cConstructing probability boxes and Dempster-Shafer structures\u201d. Sandia journal manuscript; Not yet accepted for publication. May. URL: https:\/\/www.osti.gov\/biblio\/1427258."},{"key":"2026032910310568300_ref072","first-page":"127","article-title":"Shared Certificates for Neural Network Verification","author":"Fischer","year":"2022"},{"key":"2026032910310568300_ref073","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/SP.2018.00058","article-title":"AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation","author":"Gehr","year":"2018"},{"key":"2026032910310568300_ref074","article-title":"Towards Reliable Neural Specifications","author":"Geng","year":"2022"},{"key":"2026032910310568300_ref075","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2404.04662","article-title":"Learning Minimal NAP Specifications for Neural Network Verification","volume":"abs\/2404.04662","author":"Geng","year":"2024","journal-title":"CoRR"},{"key":"2026032910310568300_ref076","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1201\/9781003162810-13","volume-title":"Low-Power Computer Vision","author":"Gholami","year":"2022"},{"key":"2026032910310568300_ref077","article-title":"A Survey of Quantization Methods for Efficient Neural Network Inference","volume":"abs\/2103.13630","author":"Gholami","year":"2021","journal-title":"CoRR"},{"key":"2026032910310568300_ref078","first-page":"627","article-title":"The Zonotope Abstract Domain Taylor1 +","author":"Ghorbal","year":"2009"},{"key":"2026032910310568300_ref079","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-030-42553-1_3","volume-title":"Case Studies in Applied Bayesian Data Science","author":"Goan","year":"2020"},{"issue":"4","key":"2026032910310568300_ref080","doi-asserted-by":"publisher","first-page":"873","DOI":"10.1145\/76359.76368","article-title":"Finding minimum-cost circulations by canceling negative cycles","volume":"36","author":"Goldberg","year":"1989","journal-title":"J. ACM"},{"key":"2026032910310568300_ref081","article-title":"Explaining and harnessing adversarial examples","volume-title":"arXiv preprint","author":"Goodfellow","year":"2014"},{"key":"2026032910310568300_ref082","first-page":"165","article-title":"Church: a language for generative models with non-parametric memoization and approximate inference","volume-title":"Uncertainty in Artificial Intelligence","author":"Goodman","year":"2008"},{"key":"2026032910310568300_ref083","unstructured":"Gopinath, D., H.Converse, C. S.Pasareanu, and A.Taly. (2020). \u201cProperty Inference for Deep Neural Networks\u201d. URL: https:\/\/arxiv.org\/abs\/1904.13215."},{"key":"2026032910310568300_ref084","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/978-3-030-88806-0_8","volume-title":"Static Analysis","author":"Goubault","year":"2021"},{"key":"2026032910310568300_ref085","first-page":"511","article-title":"Rino: Robust inner and outer approximated reachability of neural networks controlled systems","author":"Goubault","year":"2022"},{"key":"2026032910310568300_ref086","first-page":"324","article-title":"A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks","author":"Goubault","year":"2024"},{"key":"2026032910310568300_ref087","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/978-3-031-71162-6_17","volume-title":"Formal Methods","author":"Goubault","year":"2025"},{"key":"2026032910310568300_ref088","article-title":"On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models","volume":"abs\/1810.12715","author":"Gowal","year":"2018","journal-title":"CoRR"},{"key":"2026032910310568300_ref089","first-page":"4842","article-title":"Scalable verified training for provably robust image classification","author":"Gowal","year":"2019"},{"key":"2026032910310568300_ref090","doi-asserted-by":"crossref","DOI":"10.1137\/1.9780898717761","volume-title":"Evaluating derivatives: principles and techniques of algorithmic differentiation","author":"Griewank","year":"2008"},{"key":"2026032910310568300_ref091","first-page":"11536","article-title":"Pender: Incorporating shape constraints via penalized derivatives","author":"Gupta","year":"2021"},{"key":"2026032910310568300_ref092","volume-title":"Gurobi Optimizer Reference Manual","author":"Gurobi Optimization, LLC","year":"2018"},{"issue":"11","key":"2026032910310568300_ref093","doi-asserted-by":"publisher","first-page":"4310","DOI":"10.1109\/TCAD.2024.3448306","article-title":"Interval Image Abstraction for Verification of Camera-Based Autonomous Systems","volume":"43","author":"Habeeb","year":"2024","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"2026032910310568300_ref094","doi-asserted-by":"publisher","first-page":"2549","DOI":"10.24963\/ijcai.2021\/351","article-title":"DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis","author":"Henriksen","year":"2021"},{"key":"2026032910310568300_ref095","doi-asserted-by":"publisher","first-page":"2513","DOI":"10.3233\/FAIA200385","article-title":"Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search","author":"Henriksen","year":"2020"},{"key":"2026032910310568300_ref096","first-page":"2921","article-title":"Fooling Neural Network Interpretations via Adversarial Model Manipulation","volume-title":"Advances in Neural Information Processing Systems (NeurIPS)","author":"Heo","year":"2019"},{"issue":"3","key":"2026032910310568300_ref097","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/s10898-017-0537-6","article-title":"Testing pseudoconvexity via interval computation","volume":"71","author":"Hladik","year":"2018","journal-title":"Journal of Global Optimization"},{"key":"2026032910310568300_ref098","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/s10898-020-00924-w","article-title":"Linear interval parametric approach to testing pseudoconvexity","volume":"79","author":"Hladik","year":"2021","journal-title":"Journal of Global Optimization"},{"key":"2026032910310568300_ref099","doi-asserted-by":"crossref","DOI":"10.1088\/1742-6596\/16\/1\/063","article-title":"Sensitivity analysis and design optimization through automatic differentiation","author":"Hovland","year":"2005"},{"key":"2026032910310568300_ref100","article-title":"Unlocking Deterministic Robustness Certification on ImageNet","author":"Hu","year":"2023"},{"key":"2026032910310568300_ref101","first-page":"42993","article-title":"Unlocking deterministic robustness certification on imagenet","volume":"36","author":"Hu","year":"2023","journal-title":"Advances in Neural Information Processing Systems"},{"key":"2026032910310568300_ref102","first-page":"229","article-title":"Aqua: Automated quantized inference for probabilistic programs","author":"Huang","year":"2021"},{"key":"2026032910310568300_ref103","first-page":"205","article-title":"Verifying properties of differentiable programs","author":"H\u00fcckelheim","year":"2018"},{"key":"2026032910310568300_ref104","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011511","article-title":"Abduction-based explanations for Machine Learning models","author":"Ignatiev","year":"2019"},{"key":"2026032910310568300_ref105","first-page":"169","article-title":"Verisig: Verifying Safety Properties of Hybrid Systems with Neural Network Controllers","author":"Ivanov","year":"2019"},{"key":"2026032910310568300_ref106","first-page":"2017","article-title":"Spatial Transformer Networks","volume-title":"Proc. Neural Information Processing Systems (NeurIPS)","author":"Jaderberg","year":"2015"},{"key":"2026032910310568300_ref107","first-page":"4127","article-title":"Certified Robustness to Adversarial Word Substitutions","author":"Jia","year":"2019"},{"key":"2026032910310568300_ref108","unstructured":"Jiang, E. and G.Singh. (2024). \u201cTowards Universal Certified Robustness with Multi-Norm Training\u201d. URL: https:\/\/arxiv.org\/abs\/2410.03000."},{"key":"2026032910310568300_ref109","unstructured":"Jin, S., F. Y.Yan, C.Tan, A.Kalia, X.Foukas, and Z. M.Mao. (2024). \u201cAutoSpec: Automated Generation of Neural Network Specifications\u201d. URL: https:\/\/arxiv.org\/abs\/2409.10897."},{"key":"2026032910310568300_ref110","first-page":"5118","article-title":"Provable Lipschitz certification for generative models","author":"Jordan","year":"2021"},{"key":"2026032910310568300_ref111","article-title":"Exactly Computing the Local Lipschitz Constant of ReLU Networks","author":"Jordan","year":"2020"},{"key":"2026032910310568300_ref112","article-title":"On the Paradox of Certified Training","volume-title":"Trans. Mach. Learn. Res. 2022","author":"Jovanovic","year":"2022"},{"key":"2026032910310568300_ref113","first-page":"299","article-title":"Boosting Robustness Verification of Semantic Feature Neighborhoods","author":"Kabaha","year":"2022"},{"issue":"OOP-SLA1","key":"2026032910310568300_ref114","doi-asserted-by":"publisher","first-page":"1010","DOI":"10.1145\/3649847","article-title":"Verification of Neural Networks\u2019 Global Robustness","volume":"8","author":"Kabaha","year":"2024","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref115","first-page":"97","article-title":"Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks","author":"Katz","year":"2017"},{"key":"2026032910310568300_ref116","first-page":"443","volume-title":"The Marabou Framework for Verification and Analysis of Deep Neural Networks","author":"Katz","year":"2019"},{"key":"2026032910310568300_ref117","article-title":"Adam: A Method for Stochastic Optimization","author":"Kingma","year":"2015"},{"issue":"4","key":"2026032910310568300_ref118","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1561\/2200000056","article-title":"An Introduction to Variational Autoencoders","volume":"12","author":"Kingma","year":"2019","journal-title":"Foundations and Trends\u00ae in Machine Learning"},{"key":"2026032910310568300_ref119","first-page":"3468","article-title":"POPQORN: Quantifying Robustness of Recurrent Neural Networks","author":"Ko","year":"2019"},{"issue":"9","key":"2026032910310568300_ref120","doi-asserted-by":"publisher","first-page":"4043","DOI":"10.1109\/TAC.2020.3024348","article-title":"Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis","volume":"66","author":"Kochdumper","year":"2021","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026032910310568300_ref121","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-031-33170-1_2","volume-title":"NASA Formal Methods","author":"Kochdumper","year":"2023"},{"issue":"12","key":"2026032910310568300_ref122","first-page":"1","article-title":"Critically Assessing the State of the Art in Neural Network Verification","volume":"25","author":"K\u00f6nig","year":"2024","journal-title":"Journal of Machine Learning Research"},{"key":"2026032910310568300_ref123","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-03170368-3_23","article-title":"Automated Design of Linear Bounding Functions for Sigmoidal Nonlinearities in Neural Networks","author":"K\u00f6nig","year":"2024"},{"key":"2026032910310568300_ref124","first-page":"36","article-title":"Adversarial examples for generative models","author":"Kos","year":"2018"},{"key":"2026032910310568300_ref125","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2302.01404","article-title":"Provably Bounding Neural Network Preimages","volume":"abs\/2302.01404","author":"Kotha","year":"2023","journal-title":"CoRR"},{"key":"2026032910310568300_ref126","volume-title":"Learning Multiple Layers of Features from Tiny Images","author":"Krizhevsky","year":"2009"},{"key":"2026032910310568300_ref127","article-title":"Adversarial examples in the physical world","author":"Kurakin","year":"2017"},{"key":"2026032910310568300_ref128","unstructured":"Kurin, V., A. D.Palma, I.Kostrikov, S.Whiteson, and M. P.Kumar. (2022). \u201cIn Defense of the Unitary Scalarization for Deep MultiTask Learning\u201d. In: Advances in Neural Information Processing Systems. Ed. by A. H.Oh, A.Agarwal, D.Belgrave, and K.Cho. URL: https:\/\/openreview.net\/forum?id=wmwgLEPjL9."},{"key":"2026032910310568300_ref129","doi-asserted-by":"publisher","DOI":"10.1145\/3575870.3587129","article-title":"Automatic Abstraction Refinement in Neural Network Verification using Sensitivity Analysis","author":"Ladner","year":"2023"},{"key":"2026032910310568300_ref130","doi-asserted-by":"crossref","unstructured":"Ladner, T. and M.Althoff. (2024). \u201cExponent Relaxation of Polynomial Zonotopes and Its Applications in Formal Neural Network Verification\u201d. In: AAAI. 21304\u201321311. URL: https:\/\/doi.org\/10.1609\/aaai.v38i19.30125.","DOI":"10.1609\/aaai.v38i19.30125"},{"key":"2026032910310568300_ref131","unstructured":"Ladner, T., M.Eichelbeck, and M.Althoff. (2024). \u201cFormal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure\u201d. URL: https:\/\/arxiv.org\/abs\/2404.15065."},{"key":"2026032910310568300_ref132","first-page":"7272","article-title":"Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations","author":"Lan","year":"2022"},{"key":"2026032910310568300_ref133","volume-title":"Static Analysis of Differentiable Programs","author":"Laurel","year":"2024"},{"key":"2026032910310568300_ref134","doi-asserted-by":"crossref","DOI":"10.1145\/3622867","article-title":"Synthesizing Precise Static Analyzers for Automatic Differentiation","volume-title":"Proc. ACM Program. Lang. (OOPSLA2)","author":"Laurel","year":"2023"},{"key":"2026032910310568300_ref135","article-title":"Abstract Interpretation of Automatic Differentiation","author":"Laurel","year":"2024"},{"issue":"POPL","key":"2026032910310568300_ref136","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3498718","article-title":"A dual number abstraction for static analysis of Clarke Jacobians","volume":"6","author":"Laurel","year":"2022","journal-title":"Proc. ACM Program. Lang."},{"issue":"OOP-SLA2","key":"2026032910310568300_ref137","doi-asserted-by":"crossref","first-page":"1007","DOI":"10.1145\/3563324","article-title":"A general construction for abstract interpretation of higher-order automatic differentiation","volume":"6","author":"Laurel","year":"2022","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref138","first-page":"396","article-title":"Handwritten Digit Recognition with a Back-Propagation Network","volume-title":"NIPS","author":"LeCun","year":"1989"},{"key":"2026032910310568300_ref139","article-title":"Globally-Robust Neural Networks","volume":"abs\/2102.08452","author":"Leino","year":"2021","journal-title":"CoRR"},{"key":"2026032910310568300_ref140","unstructured":"Lemesle, A., J.Lehmann, and T. L.Gall. (2024). \u201cNeural Network Verification with PyRAT\u201d. URL: https:\/\/arxiv.org\/abs\/2410.23903."},{"key":"2026032910310568300_ref141","first-page":"1224","article-title":"Explaining local, global, and higher-order interactions in deep learning","author":"Lerman","year":"2021"},{"key":"2026032910310568300_ref142","first-page":"11908","article-title":"Adversarial Music: Real world Audio Adversary against Wake-word Detection System","volume-title":"Proc. Neural Information Processing Systems (NeurIPS)","author":"Li","year":"2019"},{"key":"2026032910310568300_ref143","first-page":"3896","article-title":"Adversarial camera stickers: A physical camera-based attack on deep learning systems","author":"Li","year":"2019"},{"key":"2026032910310568300_ref144","article-title":"SoK: Certified Robustness for Deep Neural Networks","volume":"abs\/2009.04131","author":"Li","year":"2020","journal-title":"CoRR"},{"key":"2026032910310568300_ref145","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1016\/j.neucom.2021.07.045","article-title":"Pruning and quantization for deep neural network acceleration: A survey","volume":"461","author":"Liang","year":"2021","journal-title":"Neurocomputing"},{"key":"2026032910310568300_ref146","article-title":"Automated Invariance Testing for Machine Learning Models Using Sparse Linear Layers","author":"Liao","year":"2022"},{"key":"2026032910310568300_ref147","article-title":"Defensive Quantization: When Efficiency Meets Robustness","author":"Lin","year":"2019"},{"key":"2026032910310568300_ref148","first-page":"91390","article-title":"NN4SysBench: Characterizing Neural Network Verification for Computer Systems","volume":"37","author":"Lin","year":"2024","journal-title":"Advances in Neural Information Processing Systems"},{"key":"2026032910310568300_ref149","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1145\/3447993.3483275","article-title":"FIRE: enabling reciprocity for FDD MIMO systems","author":"Liu","year":"2021"},{"key":"2026032910310568300_ref150","first-page":"1801","article-title":"Exploring practical vulnerabilities of machine learning-based wireless systems","author":"Liu","year":"2023"},{"key":"2026032910310568300_ref151","unstructured":"Lu, J. and M. P.Kumar. (2019). \u201cNeural Network Branching for Neural Network Verification\u201d. URL: https:\/\/arxiv.org\/abs\/1912.01329."},{"key":"2026032910310568300_ref152","article-title":"A unified approach to interpreting model predictions","volume":"abs\/1705.07874","author":"Lundberg","year":"2017","journal-title":"CoRR"},{"key":"2026032910310568300_ref153","doi-asserted-by":"crossref","unstructured":"Lyu, Z., M.Guo, T.Wu, G.Xu, K.Zhang, and D.Lin. (2021). \u201cTowards Evaluating and Training Verifiably Robust Neural Networks\u201d. URL: https:\/\/arxiv.org\/abs\/2104.00447.","DOI":"10.1109\/CVPR46437.2021.00429"},{"key":"2026032910310568300_ref154","first-page":"5037","article-title":"Fastened crown: Tightened neural network robustness certificates","author":"Lyu","year":"2020"},{"key":"2026032910310568300_ref155","first-page":"1","article-title":"A comparison of automatic differentiation and continuous sensitivity analysis for derivatives of differential equation solutions","author":"Ma","year":"2021"},{"key":"2026032910310568300_ref156","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-981-99-7584-6_17","article-title":"Verifying Neural Networks by Approximating Convex Hulls","author":"Ma","year":"2023"},{"issue":"POPL","key":"2026032910310568300_ref157","doi-asserted-by":"publisher","DOI":"10.1145\/3632917","article-title":"ReLU Hull Approximation","volume":"8","author":"Ma","year":"2024","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref158","article-title":"Towards deep learning models resistant to adversarial attacks","volume-title":"arXiv preprint","author":"Madry","year":"2017"},{"key":"2026032910310568300_ref159","doi-asserted-by":"publisher","first-page":"2658","DOI":"10.24963\/IJCAI.2021\/366","article-title":"On Guaranteed Optimal Robust Explanations for NLP Models","author":"Malfa","year":"2021"},{"key":"2026032910310568300_ref160","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-30023-3_5","article-title":"Applying automatic differentiation to the Community Land Model","volume-title":"Recent Advances in Algorithmic Differentiation","author":"Mametjanov","year":"2012"},{"key":"2026032910310568300_ref161","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-65474-0_13","article-title":"Probabilistic Lipschitz Analysis of Neural Networks","author":"Mangal","year":"2020"},{"key":"2026032910310568300_ref162","unstructured":"Mao, Y., S.Balauca, and M.Vechev. (2024). \u201cCTBENCH: A Library and Benchmark for Certified Training\u201d. URL: https:\/\/arxiv.org\/abs\/2406.04848."},{"key":"2026032910310568300_ref163","article-title":"Connecting Certified and Adversarial Training","author":"Mao","year":"2023"},{"issue":"4","key":"2026032910310568300_ref164","doi-asserted-by":"crossref","first-page":"463","DOI":"10.3233\/JCS-130469","article-title":"Dynamic enforcement of knowledge-based security policies using probabilistic abstract interpretation","volume":"21","author":"Mardziel","year":"2013","journal-title":"J. Comput. Secur."},{"key":"2026032910310568300_ref165","doi-asserted-by":"publisher","first-page":"12342","DOI":"10.1609\/AAAI.V36I11.21499","article-title":"Delivering Trustworthy AI through Formal XAI","author":"Marques-Silva","year":"2022"},{"key":"2026032910310568300_ref166","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","article-title":"A Few Graph-Based Relational Numerical Abstract Domains","author":"Mine","year":"2002"},{"issue":"1","key":"2026032910310568300_ref167","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"19","author":"Min\u00e9","year":"2006","journal-title":"High. Order Symb. Comput."},{"issue":"3-4","key":"2026032910310568300_ref168","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1561\/2500000034","article-title":"Tutorial on static inference of numeric invariants by abstract interpretation","volume":"4","author":"Mine","year":"2017","journal-title":"Foundations and Trends\u00ae in Programming Languages"},{"key":"2026032910310568300_ref169","first-page":"3578","article-title":"Differentiable abstract interpretation for provably robust neural networks","author":"Mirman","year":"2018"},{"key":"2026032910310568300_ref170","doi-asserted-by":"publisher","first-page":"1141","DOI":"10.1145\/3453483.3454100","article-title":"Robustness certification with generative models","author":"Mirman","year":"2021"},{"key":"2026032910310568300_ref171","unstructured":"Mirman, M., G.Singh, and M.Vechev. (2020). \u201cA Provable Defense for Deep Residual Networks\u201d. URL: https:\/\/arxiv.org\/abs\/1903.12519."},{"issue":"10","key":"2026032910310568300_ref172","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1145\/2714064.2660231","article-title":"Chisel: Reliability-and accuracy-aware optimization of approximate computational kernels","volume":"49","author":"Misailovic","year":"2014","journal-title":"ACM Sigplan Notices"},{"key":"2026032910310568300_ref173","doi-asserted-by":"crossref","DOI":"10.23919\/DATE56975.2023.10137324","article-title":"ViX: Analysis-driven Compiler for Efficient Low-Precision Variational Inference","author":"Misra","year":"2023"},{"issue":"2","key":"2026032910310568300_ref174","doi-asserted-by":"publisher","DOI":"10.1145\/142920.134082","article-title":"Illumination from curved reflectors","volume":"26","author":"Mitchell","year":"1992","journal-title":"SIGGRAPH Comput. Graph."},{"key":"2026032910310568300_ref175","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-031-75778-5_5","article-title":"Formal Verification Techniques for Vision-Based Autonomous Systems - A Survey","author":"Mitra","year":"2024"},{"key":"2026032910310568300_ref176","first-page":"241","article-title":"Towards Verifying Robustness of Neural Networks Against A Family of Semantic Perturbations","author":"Mohapatra","year":"2020"},{"key":"2026032910310568300_ref177","article-title":"Assessment of Neural Networks for Stream-Water-Temperature Prediction","volume":"abs\/2110.04254","author":"Mohr","year":"2021","journal-title":"CoRR"},{"key":"2026032910310568300_ref178","volume-title":"Proceedings of Machine Learning and Systems 2021, MLSys 2021, virtual, April 5-9, 2021","author":"M\u00fcller","year":"2021"},{"key":"2026032910310568300_ref179","article-title":"The third international verification of neural networks competition (VNN-COMP 2022): Summary and results","volume-title":"arXiv preprint","author":"M\u00fcller","year":"2022"},{"key":"2026032910310568300_ref180","article-title":"Certified Training: Small Boxes are All You Need","author":"M\u00fcller","year":"2023"},{"issue":"PLDI","key":"2026032910310568300_ref181","doi-asserted-by":"crossref","first-page":"786","DOI":"10.1145\/3591252","article-title":"Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks","volume":"7","author":"M\u00fcller","year":"2023","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref182","article-title":"Precise Multi-Neuron Abstractions for Neural Network Certification","volume-title":"arXiv preprint","author":"M\u00fcller","year":"2021"},{"key":"2026032910310568300_ref183","first-page":"37","article-title":"Verifying Attention Robustness of Deep Neural Networks Against Semantic Perturbations","author":"Munakata","year":"2023"},{"key":"2026032910310568300_ref184","volume-title":"Principles of program analysis","author":"Nielson","year":"2005"},{"key":"2026032910310568300_ref185","article-title":"Scaling the Convex Barrier with Active Sets","author":"Palma","year":"2021"},{"key":"2026032910310568300_ref186","article-title":"Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition","volume":"abs\/2104.06718","author":"Palma","year":"2021","journal-title":"CoRR"},{"key":"2026032910310568300_ref187","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2206.14772","article-title":"IBP Regularization for Verified Adversarial Robustness via Branch-and-Bound","volume":"abs\/2206.14772","author":"Palma","year":"2022","journal-title":"CoRR"},{"key":"2026032910310568300_ref188","article-title":"Expressive Losses for Verified Robustness via Convex Combinations","author":"Palma","year":"2024"},{"key":"2026032910310568300_ref189","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2305.12295","article-title":"Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning","volume":"abs\/2305.12295","author":"Pan","year":"2023","journal-title":"CoRR"},{"key":"2026032910310568300_ref190","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/3387939.3391594","article-title":"On the probabilistic analysis of neural networks","author":"P\u0103s\u0103reanu","year":"2020"},{"key":"2026032910310568300_ref191","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-030-99524-9_19","article-title":"LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions","author":"Paulsen","year":"2022"},{"key":"2026032910310568300_ref192","doi-asserted-by":"publisher","first-page":"714","DOI":"10.1145\/3377811.3380337","article-title":"ReluDiff: differential verification of deep neural networks","author":"Paulsen","year":"2020"},{"key":"2026032910310568300_ref193","first-page":"1","article-title":"DeepXplore: Automated Whitebox Testing of Deep Learning Systems","author":"Pei","year":"2017"},{"key":"2026032910310568300_ref194","first-page":"966","article-title":"Probabilistic Verification of ReLU Neural Networks via Characteristic Functions","author":"Pilipovsky","year":"2023"},{"key":"2026032910310568300_ref195","article-title":"Abstraction based Output Range Analysis for Neural Networks","author":"Prabhakar","year":"2019"},{"key":"2026032910310568300_ref196","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14295-6_24","article-title":"An Abstraction-Refinement Approach to Verification of Artificial Neural Networks","author":"Pulina","year":"2010"},{"key":"2026032910310568300_ref197","doi-asserted-by":"publisher","first-page":"11890","DOI":"10.1609\/AAAI.V34I07.6863","article-title":"Visualizing Deep Networks by Optimizing with Integrated Gradients","author":"Qi","year":"2020"},{"key":"2026032910310568300_ref198","first-page":"12903","article-title":"Quantifying safety of learning-based self-driving control using almost-barrier functions","author":"Qin","year":"2022"},{"key":"2026032910310568300_ref199","doi-asserted-by":"crossref","DOI":"10.21203\/rs.3.rs-55125\/v1","article-title":"Universal differential equations for scientific machine learning","volume-title":"arXiv preprint","author":"Rackauckas","year":"2020"},{"key":"2026032910310568300_ref200","first-page":"1508","article-title":"Fairness-Aware Training of Decision Trees by Abstract Interpretation","author":"Ranzato","year":"2021"},{"key":"2026032910310568300_ref201","doi-asserted-by":"crossref","unstructured":"R\u00e4uker, T., A.Ho, S.Casper, and D.Hadfield-Menell. (2023). \u201cToward Transparent AI: A Survey on Interpreting the Inner Structures of Deep Neural Networks\u201d. URL: https:\/\/arxiv.org\/abs\/2207.13243.","DOI":"10.1109\/SaTML54575.2023.00039"},{"key":"2026032910310568300_ref202","first-page":"1135","article-title":"\u201cWhy Should I Trust You?\u201d: Explaining the Predictions of Any Classifier","author":"Ribeiro","year":"2016"},{"key":"2026032910310568300_ref203","doi-asserted-by":"publisher","first-page":"1527","DOI":"10.1609\/AAAI.V32I1.11491","article-title":"Anchors: High-Precision Model-Agnostic Explanations","author":"Ribeiro","year":"2018"},{"key":"2026032910310568300_ref204","volume-title":"Introduction to static analysis: an abstract interpretation perspective","author":"Rival","year":"2020"},{"key":"2026032910310568300_ref205","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1109\/OJCSYS.2023.3265901","article-title":"Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems","volume":"2","author":"Rober","year":"2023","journal-title":"IEEE Open Journal of Control Systems"},{"key":"2026032910310568300_ref206","first-page":"5944","article-title":"Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the Hamming Distance","author":"Ruan","year":"2019"},{"key":"2026032910310568300_ref207","first-page":"225","article-title":"Scalable Polyhedral Verification of Recurrent Neural Networks","author":"Ryou","year":"2021"},{"key":"2026032910310568300_ref208","doi-asserted-by":"crossref","DOI":"10.1109\/CDC40024.2019.9029363","article-title":"Linear Encodings for Polytope Containment Problems","author":"Sadraddini","year":"2019"},{"key":"2026032910310568300_ref209","article-title":"A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks","author":"Salman","year":"2019"},{"issue":"3","key":"2026032910310568300_ref210","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1109\/JPROC.2021.3060483","article-title":"Explaining Deep Neural Networks and Beyond: A Review of Methods and Applications","volume":"109","author":"Samek","year":"2021","journal-title":"Proc. IEEE"},{"key":"2026032910310568300_ref211","first-page":"447","article-title":"Static analysis for probabilistic programs: inferring whole program properties from finitely many paths","author":"Sankaranarayanan","year":"2013"},{"issue":"2","key":"2026032910310568300_ref212","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1109\/MDAT.2020.2971217","article-title":"Robust Machine Learning Systems: Challenges, Current Trends, Perspectives, and the Road Ahead","volume":"37","author":"Shafique","year":"2020","journal-title":"IEEE Design Test"},{"issue":"POPL","key":"2026032910310568300_ref213","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3434284","article-title":"LambdaS: computable semantics for differentiable programming with higher-order functions and datatypes","volume":"5","author":"Sherman","year":"2021","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"2026032910310568300_ref214","unstructured":"Shi, Z., Q.Jin, Z.Kolter, S.Jana, C.-J.Hsieh, and H.Zhang. (2024). \u201cNeural Network Verification with Branch-and-Bound for General Nonlinearities\u201d. URL: https:\/\/arxiv.org\/abs\/2405.21063."},{"key":"2026032910310568300_ref215","article-title":"Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation","volume-title":"Advances in Neural Information Processing Systems","author":"Shi","year":"2022"},{"key":"2026032910310568300_ref216","unstructured":"Shi, Z., Y.Wang, H.Zhang, J.Yi, and C.-J.Hsieh. (2021). \u201cFast Certified Robust Training with Short Warmup\u201d. URL: https:\/\/arxiv.org\/abs\/2103.17268."},{"issue":"117","key":"2026032910310568300_ref217","first-page":"1","article-title":"Overt: An algorithm for safety verification of neural network control policies for nonlinear systems","volume":"23","author":"Sidrane","year":"2022","journal-title":"Journal of Machine Learning Research"},{"key":"2026032910310568300_ref218","first-page":"661","article-title":"Monotonic Networks","author":"Sill","year":"1997"},{"issue":"1","key":"2026032910310568300_ref219","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/s10990-010-9062-8","article-title":"The two variable per inequality abstract domain","volume":"23","author":"Simon","year":"2010","journal-title":"High. Order Symb. Comput."},{"key":"2026032910310568300_ref220","article-title":"Deep inside convolutional networks: Visualising image classification models and saliency maps","volume-title":"arXiv preprint","author":"Simonyan","year":"2013"},{"key":"2026032910310568300_ref221","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2403.18729","article-title":"ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses","volume":"abs\/2403.18729","author":"Singh","year":"2024","journal-title":"CoRR"},{"issue":"OOPSLA1","key":"2026032910310568300_ref222","doi-asserted-by":"publisher","DOI":"10.1145\/3720509","article-title":"Automated Verification of Soundness of DNN Certifiers","volume":"9","author":"Singh","year":"2025","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref223","article-title":"Beyond the single neuron convex barrier for neural network certification","volume-title":"Advances in Neural Information Processing Systems","author":"Singh","year":"2019"},{"key":"2026032910310568300_ref224","first-page":"31","article-title":"Fast and effective robustness certification","volume-title":"Advances in Neural Information Processing Systems","author":"Singh","year":"2018"},{"issue":"POPL","key":"2026032910310568300_ref225","doi-asserted-by":"crossref","DOI":"10.1145\/3290354","article-title":"An abstract domain for certifying neural networks","volume":"3","author":"Singh","year":"2019","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"2026032910310568300_ref226","article-title":"Boosting Robustness Certification of Neural Networks","author":"Singh","year":"2019"},{"key":"2026032910310568300_ref227","article-title":"Robustness Certification with Refinement","author":"Singh","year":"2019"},{"key":"2026032910310568300_ref228","first-page":"46","article-title":"Fast polyhedra abstract domain","author":"Singh","year":"2017"},{"key":"2026032910310568300_ref229","unstructured":"Singla, S. and S.Feizi. (2021). \u201cSkew Orthogonal Convolutions\u201d. URL: https:\/\/arxiv.org\/abs\/2105.11417."},{"key":"2026032910310568300_ref230","article-title":"Counterexample-guided learning of monotonic neural networks","volume-title":"Neural Information Processing Systems","author":"Sivaraman","year":"2020"},{"key":"2026032910310568300_ref231","article-title":"Smoothgrad: removing noise by adding noise","volume-title":"arXiv preprint","author":"Smilkov","year":"2017"},{"issue":"1","key":"2026032910310568300_ref232","first-page":"1929","article-title":"Dropout: a simple way to prevent neural networks from overfitting","volume":"15","author":"Srivastava","year":"2014","journal-title":"J. Mach. Learn. Res."},{"key":"2026032910310568300_ref233","article-title":"Relational Verification Leaps Forward with RABBit","author":"Suresh","year":"2024"},{"key":"2026032910310568300_ref234","article-title":"Intriguing properties of neural networks","volume-title":"ICLR (Poster)","author":"Szegedy","year":"2014"},{"key":"2026032910310568300_ref235","doi-asserted-by":"crossref","first-page":"392","DOI":"10.1007\/978-3-031-64626-3_23","volume-title":"Theoretical Aspects of Software Engineering","author":"Tang","year":"2024"},{"key":"2026032910310568300_ref236","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/978-3-031-44245-2_23","article-title":"Boosting Multi-neuron Convex Relaxation for Neural Network Verification","author":"Tang","year":"2023"},{"key":"2026032910310568300_ref237","first-page":"21675","article-title":"The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification","volume":"33","author":"Tjandraatmadja","year":"2020","journal-title":"Advances in Neural Information Processing Systems"},{"key":"2026032910310568300_ref238","first-page":"18","article-title":"Verification of Deep Convolutional Neural Networks Using ImageStars","author":"Tran","year":"2020"},{"key":"2026032910310568300_ref239","doi-asserted-by":"publisher","DOI":"10.1145\/3575870.3587112","article-title":"Quantitative Verification for Neural Networks using ProbStars","author":"Tran","year":"2023"},{"key":"2026032910310568300_ref240","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","article-title":"Star-Based Reachability Analysis of Deep Neural Networks","author":"Tran","year":"2019"},{"key":"2026032910310568300_ref241","doi-asserted-by":"crossref","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","volume-title":"Formal Methods - The Next 30 Years","author":"Tran","year":"2019"},{"issue":"4-5","key":"2026032910310568300_ref242","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s00165-021-00553-4","article-title":"Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter","volume":"33","author":"Tran","year":"2021","journal-title":"Formal Aspects Comput."},{"key":"2026032910310568300_ref243","first-page":"3","article-title":"NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems","author":"Tran","year":"2020"},{"key":"2026032910310568300_ref244","article-title":"Orthogonalizing Convolutional Layers with the Cayley Transform","volume":"abs\/2104.07167","author":"Trockman","year":"2021","journal-title":"CoRR"},{"key":"2026032910310568300_ref245","article-title":"Robustness May Be at Odds with Accuracy","author":"Tsipras","year":"2019"},{"key":"2026032910310568300_ref246","article-title":"Lipschitz-margin training: scalable certification of perturbation invariance for deep neural networks","volume-title":"Neural Information Processing Systems","author":"Tsuzuku","year":"2018"},{"issue":"PLDI","key":"2026032910310568300_ref247","doi-asserted-by":"crossref","DOI":"10.1145\/3591299","article-title":"Incremental Verification of Neural Networks","volume":"7","author":"Ugare","year":"2023","journal-title":"Proc. ACM Program. Lang."},{"issue":"OOPSLA1","key":"2026032910310568300_ref248","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3527319","article-title":"Proof transfer for fast certification of multiple approximate neural networks","volume":"6","author":"Ugare","year":"2022","journal-title":"Proc. ACM Program. Lang."},{"issue":"OOPSLA","key":"2026032910310568300_ref249","doi-asserted-by":"publisher","first-page":"185:1","DOI":"10.1145\/3428253","article-title":"Perfectly parallel fairness certification of neural networks","volume":"4","author":"Urban","year":"2020","journal-title":"Proc. ACM Program. Lang."},{"issue":"OOPSLA","key":"2026032910310568300_ref250","doi-asserted-by":"publisher","DOI":"10.1145\/3428253","article-title":"Perfectly parallel fairness certification of neural networks","volume":"4","author":"Urban","year":"2020","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref251","doi-asserted-by":"crossref","DOI":"10.1145\/2854038.2854058","article-title":"Towards automatic significance analysis for approximate computing","author":"Vassiliadis","year":"2016"},{"key":"2026032910310568300_ref252","article-title":"Efficient formal safety analysis of neural networks","volume-title":"Advances in Neural Information Processing Systems","author":"Wang","year":"2018"},{"key":"2026032910310568300_ref253","article-title":"Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification","volume-title":"arXiv preprint","author":"Wang","year":"2021"},{"key":"2026032910310568300_ref254","first-page":"1","article-title":"An Accurate EEGNet-based Motor-Imagery Brain-Computer Interface for Low-Power Edge Computing","author":"Wang","year":"2020"},{"key":"2026032910310568300_ref255","first-page":"1087","article-title":"Efficient global robustness certification of neural networks via interleaving twin-network encoding","author":"Wang","year":"2022"},{"issue":"POPL","key":"2026032910310568300_ref256","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498675","article-title":"Interval universal approximation for neural networks","volume":"6","author":"Wang","year":"2022","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref257","article-title":"A Statistical Approach to Assessing Neural Network Robustness","author":"Webb","year":"2019"},{"key":"2026032910310568300_ref258","article-title":"Building Verified Neural Networks for Computer Systems with Ouroboros","author":"Wei","year":"2023"},{"key":"2026032910310568300_ref259","first-page":"5276","article-title":"Towards fast computation of certified robustness for relu networks","author":"Weng","year":"2018"},{"issue":"8","key":"2026032910310568300_ref260","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/355586.364791","article-title":"A simple automatic derivative evaluation program","volume":"7","author":"Wengert","year":"1964","journal-title":"Communications of the ACM"},{"key":"2026032910310568300_ref261","first-page":"1198","article-title":"Probabilistic Safety for Bayesian Neural Networks","author":"Wicker","year":"2020"},{"key":"2026032910310568300_ref262","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2306.13614","article-title":"Adversarial Robustness Certification for Bayesian Neural Networks","volume":"abs\/2306.13614","author":"Wicker","year":"2023","journal-title":"CoRR"},{"key":"2026032910310568300_ref263","first-page":"5283","article-title":"Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope","author":"Wong","year":"2018"},{"key":"2026032910310568300_ref264","first-page":"11205","article-title":"Leveraging Sparse Linear Layers for Debuggable Deep Networks","author":"Wong","year":"2021"},{"key":"2026032910310568300_ref265","first-page":"8410","article-title":"Scaling provable adversarial defenses","author":"Wong","year":"2018"},{"key":"2026032910310568300_ref266","article-title":"Sustainable AI: Environmental Implications, Challenges and Opportunities","author":"Wu","year":"2022"},{"issue":"OOPSLA2","key":"2026032910310568300_ref267","doi-asserted-by":"crossref","DOI":"10.1145\/3563325","article-title":"Scalable Verification of GNN-Based Job Schedulers","volume":"6","author":"Wu","year":"2022","journal-title":"Proc. ACM Program. Lang."},{"key":"2026032910310568300_ref268","unstructured":"Wu, M., X.Li, H.Wu, and C.Barrett. (2024). \u201cBetter Verified Explanations with Applications to Incorrectness and Out-of-Distribution Detection\u201d. URL: https:\/\/arxiv.org\/abs\/2409.03060."},{"key":"2026032910310568300_ref269","first-page":"22247","article-title":"VeriX: towards verified explain-ability of deep neural networks","volume":"36","author":"Wu","year":"2023","journal-title":"Advances in neural information processing systems"},{"key":"2026032910310568300_ref270","article-title":"Support is All You Need for Certified VAE Training","author":"Xu","year":"2024"},{"key":"2026032910310568300_ref271","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-031-73650-6_14","article-title":"Cross-Input Certified Training for Universal Perturbations","author":"Xu","year":"2024"},{"key":"2026032910310568300_ref272","first-page":"1129","article-title":"Automatic perturbation analysis for scalable certified robustness and beyond","volume-title":"Proc. Neural Information Processing Systems (NeurIPS)","author":"Xu","year":"2020"},{"key":"2026032910310568300_ref273","article-title":"Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers","author":"Xu","year":"2021"},{"key":"2026032910310568300_ref274","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-031-66456-4_4","article-title":"Optimal Solution Guided Branching Strategy for Neural Network Branch and Bound Verification","author":"Xue","year":"2024"},{"key":"2026032910310568300_ref275","article-title":"Safe Neurosymbolic Learning with Differentiable Symbolic Execution","author":"Yang","year":"2022"},{"key":"2026032910310568300_ref276","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2412.10915","article-title":"C3: Learning Congestion Controllers with Formal Certificates","volume":"abs\/2412.10915","author":"Yang","year":"2024","journal-title":"CoRR"},{"key":"2026032910310568300_ref277","article-title":"Lyapunov-stable neural control for state and output feedback: A novel formulation for efficient synthesis and verification","volume-title":"arXiv preprint","author":"Yang","year":"2024"},{"key":"2026032910310568300_ref278","first-page":"389","article-title":"Improving Neural Network Verification through Spurious Region Guided Refinement","author":"Yang","year":"2021"},{"key":"2026032910310568300_ref279","article-title":"Provable Defense Against Geometric Transformations","author":"Yang","year":"2023"},{"key":"2026032910310568300_ref280","article-title":"Correctness Verification of Neural Networks","volume":"abs\/1906.01030","author":"Yang","year":"2019","journal-title":"CoRR"},{"key":"2026032910310568300_ref281","unstructured":"Yang, Z., K.Xu, B.Li, and H.Zhang. (2024c). \u201cImproving Branching in Neural Network Verification with Bound Implication Graph\u201d. URL: https:\/\/openreview.net\/forum?id=mMh4W72Hhe."},{"issue":"11","key":"2026032910310568300_ref282","doi-asserted-by":"publisher","first-page":"3898","DOI":"10.1109\/TCAD.2022.3197534","article-title":"Efficient Complete Verification of Neural Networks via Layerwised Splitting and Refinement","volume":"41","author":"Yin","year":"2022","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"2026032910310568300_ref283","unstructured":"Zelazny, T., H.Wu, C.Barrett, and G.Katz. (2022). \u201cOn Optimizing Back-Substitution Methods for Neural Network Verification\u201d. URL: https:\/\/arxiv.org\/abs\/2208.07669."},{"key":"2026032910310568300_ref284","article-title":"Towards Robustness Certification Against Universal Perturbations","author":"Zeng","year":"2023"},{"key":"2026032910310568300_ref285","first-page":"12368","article-title":"Towards Certifying L-infinity Robustness using Neural Networks with L-inf-dist Neurons","author":"Zhang","year":"2021"},{"key":"2026032910310568300_ref286","article-title":"Towards stable and efficient training of ver-ifiably robust neural networks","author":"Zhang","year":"2020"},{"key":"2026032910310568300_ref287","unstructured":"Zhang, H., S.Wang, K.Xu, L.Li, B.Li, S.Jana, C.-J.Hsieh, and J. Z.Kolter. (2022). \u201cGeneral Cutting Planes for Bound-Propagation-Based Neural Network Verification\u201d. In: Advances in Neural Information Processing Systems. Ed. by A. H.Oh, A.Agarwal, D.Belgrave, and K.Cho. URL: https:\/\/openreview.net\/forum?id=5haAJAcofjc."},{"key":"2026032910310568300_ref288","article-title":"Efficient Neural Network Robustness Certification with General Activation Functions","author":"Zhang","year":"2018"},{"key":"2026032910310568300_ref289","doi-asserted-by":"crossref","DOI":"10.1609\/aaai.v33i01.33015757","article-title":"RecurJac: An Efficient Recursive Algorithm for Bounding Jacobian Matrix of Neural Networks and Its Applications","author":"Zhang","year":"2019"},{"key":"2026032910310568300_ref290","first-page":"4879","article-title":"Interpreting Neural Network Judgments via Minimal, Stable, and Symbolic Corrections","author":"Zhang","year":"2018"},{"key":"2026032910310568300_ref291","unstructured":"Zhang, X., B.Wang, M.Kwiatkowska, and H.Zhang. (2024). \u201cPREMAP: A Unifying PREiMage APproximation Framework for Neural Networks\u201d. URL: https:\/\/arxiv.org\/abs\/2408.09262."},{"key":"2026032910310568300_ref292","first-page":"1068","article-title":"Certified Robustness to Programmable Transformations in LSTMs","author":"Zhang","year":"2021"},{"key":"2026032910310568300_ref293","article-title":"Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes","author":"Zhou","year":"2024"},{"key":"2026032910310568300_ref294","first-page":"288","article-title":"Aquasense: Automated sensitivity analysis of probabilistic programs via quantized inference","author":"Zhou","year":"2023"}],"container-title":["Foundations and Trends\u00ae in Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/8\/3-4\/250\/11044856\/2500000062en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/8\/3-4\/250\/11044856\/2500000062en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:16:48Z","timestamp":1777486608000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftpgl\/article\/8\/3-4\/250\/1328365\/Safety-and-Trust-in-Artificial-Intelligence-with"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,30]]},"references-count":294,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2025,6,30]]}},"URL":"https:\/\/doi.org\/10.1561\/2500000062","relation":{},"ISSN":["2325-1107","2325-1131"],"issn-type":[{"value":"2325-1107","type":"print"},{"value":"2325-1131","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,30]]}}}