ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses

Avaljot Singh

University of Illinois Urbana Champaign

Yasmin Sarita

University of Illinois Urbana Champaign

Charith Mendis

University of Illinois Urbana Champaign

Gagandeep Singh

University of Illinois Urbana Champaign and VMware Research

The uninterpretability of Deep Neural Networks (DNNs) hinders their deployment to safety-critical applications. Recent works have shown that Abstract-Interpretation-based formal certification techniques provide promising avenues for building trust in DNNs to some extent.
The intricate mathematical background of Abstract Interpretation poses two main challenges for the users of DNNs in developing these techniques. These are (i) easily designing the algorithms that capture the intricate DNN behavior by balancing cost vs. precision tradeoff, and (ii) maintaining the over-approximation-based soundness of these certifiers. It is important to address these challenges to push the boundaries of DNN certification.

General-purpose programming languages like C++ provide extensive functionality, however, verifying the soundness of the algorithms written in them can be impractical.
The most commonly used DNN certification libraries like auto_LiRPA and ERAN prove the correctness of their analyses. However, they consist of only a few hard-coded abstract domains and abstract transformers (or transfer functions) and do not allow the user to define new analyses. Further, these libraries can handle only specific DNN architectures.

To address these issues, we develop a declarative DSL - - that can be used to specify Abstract Interpretation-based DNN certifiers. In , programmers can easily define various existing and new abstract domains and transformers, all within just a few 10s of Lines of Code as opposed to 1000s of LOCs of existing libraries.

We also provide lightweight automatic verification, which can be used to ensure the over-approximation-based soundness of the certifier code written in for arbitrary (but bounded) DNN architectures. Using this automated verification procedure, for the first time, we can verify the soundness of state-of-the-art DNN certifiers for arbitrary DNN architectures, all within a few minutes.

We prove the soundness of our verification procedure and the completeness of a subset of .

Our code is available at <https://github.com/uiuc-focal-lab/constraintflow.git>

<concept_desc>Theory of computation Logic and verification</concept_desc>
<concept_desc>Theory of computation Operational semantics</concept_desc>

[500]Theory of computation Logic and verification
[500]Theory of computation Operational semantics

20 February 2007
[revised]12 March 2009
[accepted]5 June 2009

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

titleAI Safety Summit 2023.

titleExecutive Order on the Safe, Secure, and Trustworthy Development and Use of Artificial Intelligence.

[Abadi et al(2016)]
authorpersonMartín Abadi, personPaul Barham, personJianmin Chen, personZhifeng Chen, personAndy Davis, personJeffrey Dean, personMatthieu Devin, personSanjay Ghemawat, personGeoffrey Irving, personMichael Isard, personManjunath Kudlur, personJosh Levenberg, personRajat Monga, personSherry Moore, personDerek G. Murray, personBenoit Steiner, personPaul Tucker, personVijay Vasudevan, personPete Warden, personMartin Wicke, personYuan Yu, and personXiaoqiang Zheng. year2016.
TensorFlow: A System for Large-Scale Machine Learning. In booktitle12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). publisherUSENIX Association, addressSavannah, GA, pages265–283.

authorpersonAws Albarghouthi. year2021.
booktitleIntroduction to Neural Network Verification.
[arxiv]2109.10317 [cs.LG]

[Amato et al(2013)]
authorpersonFilippo Amato, personAlberto López, personEladia María Peña-Méndez, personPetr Vaňhara, personAleš Hampl, and personJosef Havel. year2013.
Artificial neural networks in medical diagnosis.
journalJournal of Applied Biomedicine volume11, number2 (year2013).

[Anderson et al(2019)]
authorpersonGreg Anderson, personShankara Pailoor, personIsil Dillig, and personSwarat Chaudhuri. year2019.
Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness. In booktitleProc. Programming Language Design and Implementation (PLDI). pages731–744.

[Bojarski et al(2016)]
authorpersonMariusz Bojarski, personDavide Testa, personDaniel Dworakowski, personBernhard Firner, personBeat Flepp, personPrasoon Goyal, personLarry Jackel, personMathew Monfort, personUrs Muller, personJiakai Zhang, personXin Zhang, personJake Zhao, and personKarol Zieba. year2016.
End to End Learning for Self-Driving Cars.
(date04 year2016).

[Boopathy et al(2019)]
authorpersonAkhilan Boopathy, personTsui-Wei Weng, personPin-Yu Chen, personSijia Liu, and personLuca Daniel. year2019.
CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks. In booktitleProceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence (Honolulu, Hawaii, USA) (seriesAAAI'19/IAAI'19/EAAI'19). publisherAAAI Press, Article articleno398, numpages8 pages.

[Brix et al(2023)]
authorpersonChristopher Brix, personMark Niklas Müller, personStanley Bak, personTaylor T. Johnson, and personChangliu Liu. year2023.
First Three Years of the International Verification of Neural Networks Competition (VNN-COMP).
journalCoRR  volumeabs/2301.05815 (year2023).

[Bucur et al(2011)]
authorpersonStefan Bucur, personVlad Ureche, personCristian Zamfir, and personGeorge Candea. year2011.
Parallel Symbolic Execution for Automated Real-World Software Testing. In booktitleProceedings of the Sixth Conference on Computer Systems (Salzburg, Austria) (seriesEuroSys '11). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages183–198.

[Cadar et al(2008)]
authorpersonCristian Cadar, personDaniel Dunbar, and personDawson Engler. year2008.
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In booktitleProceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (San Diego, California) (seriesOSDI'08). publisherUSENIX Association, addressUSA, pages209–224.

[Cadar et al(2006)]
authorpersonCristian Cadar, personVijay Ganesh, personPeter M. Pawlowski, personDavid L. Dill, and personDawson R. Engler. year2006.
EXE: Automatically Generating Inputs of Death. In booktitleProceedings of the 13th ACM Conference on Computer and Communications Security (Alexandria, Virginia, USA) (seriesCCS '06). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages322–335.

[Chipounov et al(2012)]
authorpersonVitaly Chipounov, personVolodymyr Kuznetsov, and personGeorge Candea. year2012.
The S2E Platform: Design, Implementation, and Applications.
journalACM Trans. Comput. Syst. volume30, number1, Article articleno2 (datefeb year2012), numpages49 pages.

[Cousot and Cousot(1977)]
authorpersonPatrick Cousot and personRadhia Cousot. year1977.
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In booktitleProceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California) (seriesPOPL '77). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages238–252.

[Cousot et al(2019)]
authorpersonPatrick Cousot, personRoberto Giacobazzi, and personFrancesco Ranzato. year2019.
A²I: Abstract² Interpretation.
journalProc. ACM Program. Lang. volume3, numberPOPL, Article articleno42 (datejan year2019), numpages31 pages.

[Dario Guidotti and Pulina(2023)]
authorpersonArmando Tacchella Dario Guidotti, Stefano Demarchi and personLuca Pulina. year2023.
titleThe Verification of Neural Networks Library (VNN-LIB).
<https://www.vnnlib.org, 2023>.

[de Moura and Bjørner(2008)]
authorpersonLeonardo Mendonça de Moura and personNikolaj Bjørner. year2008.
Z3: An Efficient SMT Solver. In booktitleTACAS (seriesLecture Notes in Computer Science, Vol. volume4963). publisherSpringer, pages337–340.

[D'Souza et al(2017)]
authorpersonDeepak D'Souza, personP. Ezudheen, personPranav Garg, personP. Madhusudan, and personDaniel Neider. year2017.
Horn-ICE Learning for Synthesizing Invariants and Contracts.
journalCoRR  volumeabs/1712.09418 (year2017).

[Duong et al(2023)]
authorpersonHai Duong, personLinhan Li, personThanhVu Nguyen, and personMatthew Dwyer. year2023.
A DPLL(T) Framework for Verifying Deep Neural Networks.
journalArXiv  volumeabs/2307.10266 (year2023).

[Dutta et al(2018)]
authorpersonSouradeep Dutta, personSusmit Jha, personSriram Sankaranarayanan, and personAshish Tiwari. year2018.
Output Range Analysis for Deep Feedforward Neural Networks. In booktitleNASA Formal Methods, editorpersonAaron Dutle, personCésar Muñoz, and personAnthony Narkawicz (Eds.). publisherSpringer International Publishing, addressCham, pages121–138.

authorpersonRuediger Ehlers. year2017.
Formal verification of piece-wise linear feed-forward neural networks. In booktitleInternational Symposium on Automated Technology for Verification and Analysis.

[Ezudheen et al(2018)]
authorpersonP. Ezudheen, personDaniel Neider, personDeepak D'Souza, personPranav Garg, and personP. Madhusudan. year2018.
Horn-ICE learning for synthesizing invariants and contracts.
journalProc. ACM Program. Lang. volume2, numberOOPSLA (year2018), pages131:1–131:25.

[Gao et al(2012)]
authorpersonSicun Gao, personJeremy Avigad, and personEdmund M. Clarke. year2012.
$\delta$-Complete Decision Procedures for Satisfiability over the Reals. In booktitleInternational Joint Conference on Automated Reasoning.

[Garg et al(2014)]
authorpersonPranav Garg, personChristof Löding, personP. Madhusudan, and personDaniel Neider. year2014.
ICE: A Robust Framework for Learning Invariants. In booktitleComputer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (seriesLecture Notes in Computer Science, Vol. volume8559), editorpersonArmin Biere and personRoderick Bloem (Eds.). publisherSpringer, pages69–87.

[Gehr et al(2018)]
authorpersonTimon Gehr, personMatthew Mirman, personDana Drachsler-Cohen, personPetar Tsankov, personSwarat Chaudhuri, and personMartin T. Vechev. year2018.
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In booktitle2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA. pages3–18.

[Geng et al(2023)]
authorpersonChuqin Geng, personNham Le, personXiaojie Xu, personZhaoyue Wang, personArie Gurfinkel, and personXujie Si. year2023.
Towards Reliable Neural Specifications. In booktitleProceedings of the 40th International Conference on Machine Learning (Honolulu, Hawaii, USA) (seriesICML'23). publisherJMLR.org, Article articleno449, numpages17 pages.

[Godefroid et al(2005)]
authorpersonPatrice Godefroid, personNils Klarlund, and personKoushik Sen. year2005.
DART: Directed Automated Random Testing. In booktitleProceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (Chicago, IL, USA) (seriesPLDI '05). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages213–223.

[Huang et al(2017)]
authorpersonXiaowei Huang, personMarta Kwiatkowska, personSen Wang, and personMin Wu. year2017.
Safety Verification of Deep Neural Networks. In booktitleComputer Aided Verification, editorpersonRupak Majumdar and personViktor Kunčak (Eds.). publisherSpringer International Publishing, addressCham, pages3–29.

[Isac et al(2023)]
authorpersonOmri Isac, personYoni Zohar, personClark W. Barrett, and personGuy Katz. year2023.
DNN Verification, Reachability, and the Exponential Function Problem.
journalCoRR  volumeabs/2305.06064 (year2023).

[Jaffar et al(2012a)]
authorpersonJoxan Jaffar, personVijayaraghavan Murali, personJorge A. Navas, and personAndrew E. Santosa. year2012a.
TRACER: A Symbolic Execution Tool for Verification. In booktitleComputer Aided Verification, editorpersonP. Madhusudan and personSanjit A. Seshia (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages758–766.

[Jaffar et al(2012b)]
authorpersonJoxan Jaffar, personJorge A. Navas, and personAndrew E. Santosa. year2012b.
Unbounded Symbolic Execution for Program Verification. In booktitleRuntime Verification, editorpersonSarfraz Khurshid and personKoushik Sen (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages396–411.

[Jaffar et al(2009)]
authorpersonJoxan Jaffar, personAndrew E. Santosa, and personRăzvan Voicu. year2009.
An Interpolation Method for CLP Traversal. In booktitlePrinciples and Practice of Constraint Programming - CP 2009, editorpersonIan P. Gent (Ed.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages454–469.

[Katz et al(2019)]
authorpersonGuy Katz, personDerek Huang, personDuligur Ibeling, personKyle Julian, personChristopher Lazarus, personRachel Lim, personParth Shah, personShantanu Thakoor, personHaoze Wu, personAleksandar Zeljić, personDavid Dill, personMykel Kochenderfer, and personClark Barrett. year2019.
booktitleThe Marabou Framework for Verification and Analysis of Deep Neural Networks.

[Keuchel et al(2022)]
authorpersonSteven Keuchel, personSander Huyghebaert, personGeorgy Lukyanov, and personDominique Devriese. year2022.
Verified Symbolic Execution with Kripke Specification Monads (and No Meta-Programming).
journalProc. ACM Program. Lang. volume6, numberICFP, Article articleno97 (dateaug year2022), numpages31 pages.

[Khanh and Ogawa(2012)]
authorpersonTo Van Khanh and personMizuhito Ogawa. year2012.
SMT for Polynomial Constraints on Real Numbers. In booktitleTAPAS@SAS.

[Khurshid et al(2003)]
authorpersonSarfraz Khurshid, personCorina S. PĂsĂreanu, and personWillem Visser. year2003.
Generalized Symbolic Execution for Model Checking and Testing. In booktitleTools and Algorithms for the Construction and Analysis of Systems, editorpersonHubert Garavel and personJohn Hatcliff (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages553–568.

[Li et al(2023)]
authorpersonLinyi Li, personTao Xie, and personBo Li. year2023.
SoK: Certified Robustness for Deep Neural Networks. In booktitle44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, 22-26 May 2023. publisherIEEE.

[Lin et al(2023)]
authorpersonZhengyao Lin, personXiaohong Chen, personMinh-Thai Trinh, personJohn Wang, and personGrigore Roşu. year2023.
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier.
journalProc. ACM Program. Lang. volume7, numberOOPSLA1, Article articleno77 (dateapr year2023), numpages29 pages.

[Lorenz et al(2021)]
authorpersonT. Lorenz, personA. Ruoss, personM. Balunovic, personG. Singh, and personM. Vechev. year2021.
Robustness Certification for Point Cloud Models. In booktitle2021 IEEE/CVF International Conference on Computer Vision (ICCV). publisherIEEE Computer Society, addressLos Alamitos, CA, USA, pages7588–7598.

[Lyu et al(2020)]
authorpersonZhaoyang Lyu, personChing-Yun Ko, personZhifeng Kong, personNgai Wong, personDahua Lin, and personLuca Daniel. year2020.
Fastened CROWN: Tightened Neural Network Robustness Certificates. In booktitleThe Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. publisherAAAI Press, pages5037–5044.

[Madry et al(2018)]
authorpersonAleksander Madry, personAleksandar Makelov, personLudwig Schmidt, personDimitris Tsipras, and personAdrian Vladu. year2018.
Towards Deep Learning Models Resistant to Adversarial Attacks. In booktitleInternational Conference on Learning Representations.

authorpersonKenneth L. McMillan. year2010.
Lazy Annotation for Program Testing and Verification. In booktitleComputer Aided Verification, editorpersonTayssir Touili, personByron Cook, and personPaul Jackson (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages104–118.

[Müller et al(2021)]
authorpersonChristoph Müller, personFrançois Serre, personGagandeep Singh, personMarkus Püschel, and personMartin T. Vechev. year2021.
Scaling Polyhedral Neural Network Verification on GPUs. In booktitleProceedings of Machine Learning and Systems 2021, MLSys 2021, virtual, April 5-9, 2021, editorpersonAlex Smola, personAlex Dimakis, and personIon Stoica (Eds.). publishermlsys.org.

[Paszke et al(2019)]
authorpersonAdam Paszke, personSam Gross, personFrancisco Massa, personAdam Lerer, personJames Bradbury, personGregory Chanan, personTrevor Killeen, personZeming Lin, personNatalia Gimelshein, personLuca Antiga, personAlban Desmaison, personAndreas Köpf, personEdward Yang, personZach DeVito, personMartin Raison, personAlykhan Tejani, personSasank Chilamkurthy, personBenoit Steiner, personLu Fang, personJunjie Bai, and personSoumith Chintala. year2019.
booktitlePyTorch: An Imperative Style, High-Performance Deep Learning Library.
publisherCurran Associates Inc., addressRed Hook, NY, USA.

[Pham et al(2020)]
authorpersonLong H. Pham, personJiaying Li, and personJun Sun. year2020.
SOCRATES: Towards a Unified Platform for Neural Network Verification.
journalArXiv  volumeabs/2007.11206 (year2020).

[Raghunathan et al(2018)]
authorpersonAditi Raghunathan, personJacob Steinhardt, and personPercy Liang. year2018.
Semidefinite Relaxations for Certifying Robustness to Adversarial Examples. In booktitleProceedings of the 32nd International Conference on Neural Information Processing Systems (Montréal, Canada) (seriesNIPS'18). publisherCurran Associates Inc., addressRed Hook, NY, USA, pages10900–10910.

[Salman et al(2019)]
authorpersonHadi Salman, personGreg Yang, personHuan Zhang, personCho-Jui Hsieh, and personPengchuan Zhang. year2019.
booktitleA Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks.
publisherCurran Associates Inc., addressRed Hook, NY, USA.

[Scott et al(2022)]
authorpersonJoseph Scott, personGuanting Pan, personElias B. Khalil, and personVijay Ganesh. year2022.
Goose: A Meta-Solver for Deep Neural Network Verification. In booktitleProceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, August 11-12, 2022 (seriesCEUR Workshop Proceedings, Vol. volume3185), editorpersonDavid Déharbe and personAntti E. J. Hyvärinen (Eds.). publisherCEUR-WS.org, pages99–113.

[Sen et al(2005)]
authorpersonKoushik Sen, personDarko Marinov, and personGul Agha. year2005.
CUTE: A Concolic Unit Testing Engine for C. In booktitleProceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (Lisbon, Portugal) (seriesESEC/FSE-13). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages263–272.

[Shriver et al(2021)]
authorpersonDavid Shriver, personSebastian Elbaum, and personMatthew B. Dwyer. year2021.
DNNV: A Framework for Deep Neural Network Verification. In booktitleComputer Aided Verification, editorpersonAlexandra Silva and personK. Rustan M. Leino (Eds.). publisherSpringer International Publishing, addressCham, pages137–150.

[Si et al(2018)]
authorpersonXujie Si, personHanjun Dai, personMukund Raghothaman, personMayur Naik, and personLe Song. year2018.
Learning Loop Invariants for Program Verification. In booktitleAdvances in Neural Information Processing Systems, editorpersonS. Bengio, personH. Wallach, personH. Larochelle, personK. Grauman, personN. Cesa-Bianchi, and personR. Garnett (Eds.), Vol. volume31. publisherCurran Associates, Inc.

[Singh et al(2019a)]
authorpersonGagandeep Singh, personRupanshu Ganvir, personMarkus Püschel, and personMartin Vechev. year2019a.
booktitleBeyond the Single Neuron Convex Barrier for Neural Network Certification.
publisherCurran Associates Inc., addressRed Hook, NY, USA.

[Singh et al(2018a)]
authorpersonGagandeep Singh, personTimon Gehr, personMatthew Mirman, personMarkus Püschel, and personMartin Vechev. year2018a.
Fast and effective robustness certification.
journalAdvances in Neural Information Processing Systems  volume31 (year2018).

[Singh et al(2019b)]
authorpersonGagandeep Singh, personTimon Gehr, personMarkus Püschel, and personMartin Vechev. year2019b.
An abstract domain for certifying neural networks.
journalProceedings of the ACM on Programming Languages volume3, numberPOPL (year2019).

[Singh et al(2018b)]
authorpersonGagandeep Singh, personTimon Gehr, personMarkus Püschel, and personMartin T. Vechev. year2018b.
Boosting Robustness Certification of Neural Networks. In booktitleInternational Conference on Learning Representations.

[Singh et al(2018c)]
authorpersonGagandeep Singh, personTimon Gehr, personMarkus Püschel, and personMartin T. Vechev. year2018c.
titleETH Robustness Analyzer for Neural Networks (ERAN).

[Singh et al(2018d)]
authorpersonGagandeep Singh, personJingxuan He, personChristoph Müller, personFrançois Serre, personAnian Ruoss, personGleb Makarchuk, personMarkus Püschel, and personMartin T. Vechev. year2018d.
titleELINA: ETH LIbrary for Numerical Analysis.

[Singh et al(2017)]
authorpersonGagandeep Singh, personMarkus Püschel, and personMartin Vechev. year2017.
Fast Polyhedra Abstract Domain. In booktitleProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (seriesPOPL '17). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages46–59.

[Sotoudeh et al(2023)]
authorpersonMatthew Sotoudeh, personZhe Tao, and personAditya Thakur. year2023.
SyReNN: A tool for analyzing deep neural networks.
journalInternational Journal on Software Tools for Technology Transfer  volume25 (date02 year2023), pages1–21.

[Tjandraatmadja et al(2020)]
authorpersonChristian Tjandraatmadja, personRoss Anderson, personJoey Huchette, personWill Ma, personKrunal Patel, and personJuan Pablo Vielma. year2020.
The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification. In booktitleProceedings of the 34th International Conference on Neural Information Processing Systems (Vancouver, BC, Canada) (seriesNIPS'20). publisherCurran Associates Inc., addressRed Hook, NY, USA, Article articleno1819, numpages12 pages.

[Tjeng et al(2019)]
authorpersonVincent Tjeng, personKai Yuanqing Xiao, and personRuss Tedrake. year2019.
Evaluating Robustness of Neural Networks with Mixed Integer Programming. In booktitle7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. publisherOpenReview.net.

[Torlak and Bodik(2013)]
authorpersonEmina Torlak and personRastislav Bodik. year2013.
Growing Solver-Aided Languages with Rosette. In booktitleProceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Indianapolis, Indiana, USA) (seriesOnward! 2013). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages135–152.

[Torlak and Bodik(2014)]
authorpersonEmina Torlak and personRastislav Bodik. year2014.
A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages.
journalSIGPLAN Not. volume49, number6 (datejun year2014), pages530–541.

[Tran et al(2020)]
authorpersonHoang-Dung Tran, personStanley Bak, personWeiming Xiang, and personTaylor T. Johnson. year2020.
Verification of Deep Convolutional Neural Networks Using ImageStars. In booktitleComputer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I (Los Angeles, CA, USA). publisherSpringer-Verlag, addressBerlin, Heidelberg, pages18–42.

[Tran et al(2019)]
authorpersonHoang-Dung Tran, personDiago Manzanas Lopez, personPatrick Musau, personXiaodong Yang, personLuan Viet Nguyen, personWeiming Xiang, and personTaylor T. Johnson. year2019.
Star-Based Reachability Analysis of Deep Neural Networks. In booktitleFormal Methods – The Next 30 Years, editorpersonMaurice H. ter Beek, personAnnabelle McIver, and personJosé N. Oliveira (Eds.). publisherSpringer International Publishing, addressCham, pages670–686.

[Ugare et al(2023)]
authorpersonShubham Ugare, personDebangshu Banerjee, personSasa Misailovic, and personGagandeep Singh. year2023.
Incremental Verification of Neural Networks.
journalProc. ACM Program. Lang. volume7, numberPLDI, Article articleno185 (datejun year2023), numpages26 pages.

[Ugare et al(2022)]
authorpersonShubham Ugare, personGagandeep Singh, and personSasa Misailovic. year2022.
Proof transfer for fast certification of multiple approximate neural networks.
journalProc. ACM Program. Lang. volume6, numberOOPSLA1, Article articleno75 (dateapr year2022), numpages29 pages.

[Urban et al(2020)]
authorpersonCaterina Urban, personMaria Christakis, personValentin Wüstholz, and personFuyuan Zhang. year2020.
Perfectly Parallel Fairness Certification of Neural Networks.
journalProc. ACM Program. Lang. volume4, numberOOPSLA, Article articleno185 (datenov year2020), numpages30 pages.

[Vishwanathan et al(2023)]
authorpersonHarishankar Vishwanathan, personMatan Shachnai, personSrinivas Narayana, and personSantosh Nagarakatte. year2023.
Verifying the Verifier: eBPF Range Analysis Verification. In booktitleComputer Aided Verification.

[Visser et al(2004)]
authorpersonWillem Visser, personCorina S. Pundefinedsundefinedreanu, and personSarfraz Khurshid. year2004.
Test Input Generation with Java PathFinder. In booktitleProceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis (Boston, Massachusetts, USA) (seriesISSTA '04). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages97–107.

[Wang et al(2018a)]
authorpersonShiqi Wang, personKexin Pei, personJustin Whitehouse, personJunfeng Yang, and personSuman Jana. year2018a.
Efficient formal safety analysis of neural networks. In booktitleAdvances in Neural Information Processing Systems.

[Wang et al(2018b)]
authorpersonShiqi Wang, personKexin Pei, personJustin Whitehouse, personJunfeng Yang, and personSuman Jana. year2018b.
Formal Security Analysis of Neural Networks Using Symbolic Intervals. In booktitleProceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (seriesSEC'18). publisherUSENIX Association, addressUSA, pages1599–1614.

[Wang et al(2018c)]
authorpersonShiqi Wang, personKexin Pei, personJustin Whitehouse, personJunfeng Yang, and personSuman Jana. year2018c.
Formal Security Analysis of Neural Networks Using Symbolic Intervals. In booktitleProceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (seriesSEC'18). publisherUSENIX Association, addressUSA, pages1599–1614.

[Wang et al(2021)]
authorpersonShiqi Wang, personHuan Zhang, personKaidi Xu, personXue Lin, personSuman Jana, personCho-Jui Hsieh, and personJ Zico Kolter. year2021.
Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification.
journalarXiv preprint arXiv:2103.06624 (year2021).

[Weng et al(2018)]
authorpersonLily Weng, personHuan Zhang, personHongge Chen, personZhao Song, personCho-Jui Hsieh, personLuca Daniel, personDuane Boning, and personInderjit Dhillon. year2018.
Towards Fast Computation of Certified Robustness for ReLU Networks. In booktitleProceedings of the 35th International Conference on Machine Learning (seriesProceedings of Machine Learning Research, Vol. volume80), editorpersonJennifer Dy and personAndreas Krause (Eds.). publisherPMLR, pages5276–5285.

[Wong and Kolter(2018)]
authorpersonEric Wong and personJ. Zico Kolter. year2018.
Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In booktitleProceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, July 10-15, 2018 (seriesProceedings of Machine Learning Research, Vol. volume80), editorpersonJennifer G. Dy and personAndreas Krause (Eds.). publisherPMLR, pages5283–5292.

[Wu et al(2022)]
authorpersonHaoze Wu, personClark Barrett, personMahmood Sharif, personNina Narodytska, and personGagandeep Singh. year2022.
Scalable Verification of GNN-Based Job Schedulers.
journalProc. ACM Program. Lang. volume6, numberOOPSLA2, Article articleno162 (dateoct year2022), numpages30 pages.

[Wu et al(2020)]
authorpersonHaoze Wu, personAlex Ozdemir, personAleksandar Zeljić, personKyle Julian, personAhmed Irfan, personDivya Gopinath, personSadjad Fouladi, personGuy Katz, personCorina Pasareanu, and personClark Barrett. year2020.
Parallelization Techniques for Verifying Neural Networks. In booktitle2020 Formal Methods in Computer Aided Design (FMCAD). pages128–137.

[Xiang et al(2017)]
authorpersonWeiming Xiang, personHoang-Dung Tran, and personTaylor T. Johnson. year2017.
Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks.
journalCoRR  volumeabs/1708.03322 (year2017).

[Xu and Singh(2023)]
authorpersonChangming Xu and personGagandeep Singh. year2023.
titleRobust Universal Adversarial Perturbations.

[Xu et al(2020a)]
authorpersonKaidi Xu, personZhouxing Shi, personHuan Zhang, personYihan Wang, personKai-Wei Chang, personMinlie Huang, personBhavya Kailkhura, personXue Lin, and personCho-Jui Hsieh. year2020a.
Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond.

[Xu et al(2018)]
authorpersonKaidi Xu, personZhouxing Shi, personHuan Zhang, personYihan Wang, personKai-Wei Chang, personMinlie Huang, personBhavya Kailkhura, personXue Lin, and personCho-Jui Hsieh. year2018.
titleauto_LiRPA: An Automatic Linear Relaxation-based Perturbation Analysis Library for Neural Networks and General Computational Graphs.

[Xu et al(2020b)]
authorpersonKaidi Xu, personHuan Zhang, personShiqi Wang, personYihan Wang, personSuman Sekhar Jana, personXue Lin, and personCho-Jui Hsieh. year2020b.
Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers.
journalArXiv  volumeabs/2011.13824 (year2020).

[Yang et al(2021)]
authorpersonPengfei Yang, personRenjue Li, personJianlin Li, personCheng-Chao Huang, personJingyi Wang, personJun Sun, personBai Xue, and personLijun Zhang. year2021.
booktitleImproving Neural Network Verification through Spurious Region Guided Refinement.

[Zelazny et al(2022)]
authorpersonTom Zelazny, personHaoze Wu, personClark W. Barrett, and personGuy Katz. year2022.
On Optimizing Back-Substitution Methods for Neural Network Verification.
journal2022 Formal Methods in Computer-Aided Design (FMCAD) (year2022), pages17–26.

[Zhang et al(2018)]
authorpersonHuan Zhang, personTsui-Wei Weng, personPin-Yu Chen, personCho-Jui Hsieh, and personLuca Daniel. year2018.
Efficient Neural Network Robustness Certification with General Activation Functions. In booktitleProceedings of the 32nd International Conference on Neural Information Processing Systems (seriesNIPS'18). publisherCurran Associates Inc., addressRed Hook, NY, USA, pages4944–4953.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

titleAI Safety Summit 2023.

titleExecutive Order on the Safe, Secure, and Trustworthy Development and Use of Artificial Intelligence.

[Abadi et al(2016)]
authorpersonMartín Abadi, personPaul Barham, personJianmin Chen, personZhifeng Chen, personAndy Davis, personJeffrey Dean, personMatthieu Devin, personSanjay Ghemawat, personGeoffrey Irving, personMichael Isard, personManjunath Kudlur, personJosh Levenberg, personRajat Monga, personSherry Moore, personDerek G. Murray, personBenoit Steiner, personPaul Tucker, personVijay Vasudevan, personPete Warden, personMartin Wicke, personYuan Yu, and personXiaoqiang Zheng. year2016.
TensorFlow: A System for Large-Scale Machine Learning. In booktitle12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). publisherUSENIX Association, addressSavannah, GA, pages265–283.

authorpersonAws Albarghouthi. year2021.
booktitleIntroduction to Neural Network Verification.
[arxiv]2109.10317 [cs.LG]

[Amato et al(2013)]
authorpersonFilippo Amato, personAlberto López, personEladia María Peña-Méndez, personPetr Vaňhara, personAleš Hampl, and personJosef Havel. year2013.
Artificial neural networks in medical diagnosis.
journalJournal of Applied Biomedicine volume11, number2 (year2013).

[Anderson et al(2019)]
authorpersonGreg Anderson, personShankara Pailoor, personIsil Dillig, and personSwarat Chaudhuri. year2019.
Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness. In booktitleProc. Programming Language Design and Implementation (PLDI). pages731–744.

[Bojarski et al(2016)]
authorpersonMariusz Bojarski, personDavide Testa, personDaniel Dworakowski, personBernhard Firner, personBeat Flepp, personPrasoon Goyal, personLarry Jackel, personMathew Monfort, personUrs Muller, personJiakai Zhang, personXin Zhang, personJake Zhao, and personKarol Zieba. year2016.
End to End Learning for Self-Driving Cars.
(date04 year2016).

[Boopathy et al(2019)]
authorpersonAkhilan Boopathy, personTsui-Wei Weng, personPin-Yu Chen, personSijia Liu, and personLuca Daniel. year2019.
CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks. In booktitleProceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence (Honolulu, Hawaii, USA) (seriesAAAI'19/IAAI'19/EAAI'19). publisherAAAI Press, Article articleno398, numpages8 pages.

[Brix et al(2023)]
authorpersonChristopher Brix, personMark Niklas Müller, personStanley Bak, personTaylor T. Johnson, and personChangliu Liu. year2023.
First Three Years of the International Verification of Neural Networks Competition (VNN-COMP).
journalCoRR  volumeabs/2301.05815 (year2023).

[Bucur et al(2011)]
authorpersonStefan Bucur, personVlad Ureche, personCristian Zamfir, and personGeorge Candea. year2011.
Parallel Symbolic Execution for Automated Real-World Software Testing. In booktitleProceedings of the Sixth Conference on Computer Systems (Salzburg, Austria) (seriesEuroSys '11). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages183–198.

[Cadar et al(2008)]
authorpersonCristian Cadar, personDaniel Dunbar, and personDawson Engler. year2008.
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In booktitleProceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (San Diego, California) (seriesOSDI'08). publisherUSENIX Association, addressUSA, pages209–224.

[Cadar et al(2006)]
authorpersonCristian Cadar, personVijay Ganesh, personPeter M. Pawlowski, personDavid L. Dill, and personDawson R. Engler. year2006.
EXE: Automatically Generating Inputs of Death. In booktitleProceedings of the 13th ACM Conference on Computer and Communications Security (Alexandria, Virginia, USA) (seriesCCS '06). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages322–335.

[Chipounov et al(2012)]
authorpersonVitaly Chipounov, personVolodymyr Kuznetsov, and personGeorge Candea. year2012.
The S2E Platform: Design, Implementation, and Applications.
journalACM Trans. Comput. Syst. volume30, number1, Article articleno2 (datefeb year2012), numpages49 pages.

[Cousot and Cousot(1977)]
authorpersonPatrick Cousot and personRadhia Cousot. year1977.
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In booktitleProceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California) (seriesPOPL '77). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages238–252.

[Cousot et al(2019)]
authorpersonPatrick Cousot, personRoberto Giacobazzi, and personFrancesco Ranzato. year2019.
A²I: Abstract² Interpretation.
journalProc. ACM Program. Lang. volume3, numberPOPL, Article articleno42 (datejan year2019), numpages31 pages.

[Dario Guidotti and Pulina(2023)]
authorpersonArmando Tacchella Dario Guidotti, Stefano Demarchi and personLuca Pulina. year2023.
titleThe Verification of Neural Networks Library (VNN-LIB).
<https://www.vnnlib.org, 2023>.

[de Moura and Bjørner(2008)]
authorpersonLeonardo Mendonça de Moura and personNikolaj Bjørner. year2008.
Z3: An Efficient SMT Solver. In booktitleTACAS (seriesLecture Notes in Computer Science, Vol. volume4963). publisherSpringer, pages337–340.

[D'Souza et al(2017)]
authorpersonDeepak D'Souza, personP. Ezudheen, personPranav Garg, personP. Madhusudan, and personDaniel Neider. year2017.
Horn-ICE Learning for Synthesizing Invariants and Contracts.
journalCoRR  volumeabs/1712.09418 (year2017).

[Duong et al(2023)]
authorpersonHai Duong, personLinhan Li, personThanhVu Nguyen, and personMatthew Dwyer. year2023.
A DPLL(T) Framework for Verifying Deep Neural Networks.
journalArXiv  volumeabs/2307.10266 (year2023).

[Dutta et al(2018)]
authorpersonSouradeep Dutta, personSusmit Jha, personSriram Sankaranarayanan, and personAshish Tiwari. year2018.
Output Range Analysis for Deep Feedforward Neural Networks. In booktitleNASA Formal Methods, editorpersonAaron Dutle, personCésar Muñoz, and personAnthony Narkawicz (Eds.). publisherSpringer International Publishing, addressCham, pages121–138.

authorpersonRuediger Ehlers. year2017.
Formal verification of piece-wise linear feed-forward neural networks. In booktitleInternational Symposium on Automated Technology for Verification and Analysis.

[Ezudheen et al(2018)]
authorpersonP. Ezudheen, personDaniel Neider, personDeepak D'Souza, personPranav Garg, and personP. Madhusudan. year2018.
Horn-ICE learning for synthesizing invariants and contracts.
journalProc. ACM Program. Lang. volume2, numberOOPSLA (year2018), pages131:1–131:25.

[Gao et al(2012)]
authorpersonSicun Gao, personJeremy Avigad, and personEdmund M. Clarke. year2012.
$\delta$-Complete Decision Procedures for Satisfiability over the Reals. In booktitleInternational Joint Conference on Automated Reasoning.

[Garg et al(2014)]
authorpersonPranav Garg, personChristof Löding, personP. Madhusudan, and personDaniel Neider. year2014.
ICE: A Robust Framework for Learning Invariants. In booktitleComputer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (seriesLecture Notes in Computer Science, Vol. volume8559), editorpersonArmin Biere and personRoderick Bloem (Eds.). publisherSpringer, pages69–87.

[Gehr et al(2018)]
authorpersonTimon Gehr, personMatthew Mirman, personDana Drachsler-Cohen, personPetar Tsankov, personSwarat Chaudhuri, and personMartin T. Vechev. year2018.
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In booktitle2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA. pages3–18.

[Geng et al(2023)]
authorpersonChuqin Geng, personNham Le, personXiaojie Xu, personZhaoyue Wang, personArie Gurfinkel, and personXujie Si. year2023.
Towards Reliable Neural Specifications. In booktitleProceedings of the 40th International Conference on Machine Learning (Honolulu, Hawaii, USA) (seriesICML'23). publisherJMLR.org, Article articleno449, numpages17 pages.

[Godefroid et al(2005)]
authorpersonPatrice Godefroid, personNils Klarlund, and personKoushik Sen. year2005.
DART: Directed Automated Random Testing. In booktitleProceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (Chicago, IL, USA) (seriesPLDI '05). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages213–223.

[Huang et al(2017)]
authorpersonXiaowei Huang, personMarta Kwiatkowska, personSen Wang, and personMin Wu. year2017.
Safety Verification of Deep Neural Networks. In booktitleComputer Aided Verification, editorpersonRupak Majumdar and personViktor Kunčak (Eds.). publisherSpringer International Publishing, addressCham, pages3–29.

[Isac et al(2023)]
authorpersonOmri Isac, personYoni Zohar, personClark W. Barrett, and personGuy Katz. year2023.
DNN Verification, Reachability, and the Exponential Function Problem.
journalCoRR  volumeabs/2305.06064 (year2023).

[Jaffar et al(2012a)]
authorpersonJoxan Jaffar, personVijayaraghavan Murali, personJorge A. Navas, and personAndrew E. Santosa. year2012a.
TRACER: A Symbolic Execution Tool for Verification. In booktitleComputer Aided Verification, editorpersonP. Madhusudan and personSanjit A. Seshia (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages758–766.

[Jaffar et al(2012b)]
authorpersonJoxan Jaffar, personJorge A. Navas, and personAndrew E. Santosa. year2012b.
Unbounded Symbolic Execution for Program Verification. In booktitleRuntime Verification, editorpersonSarfraz Khurshid and personKoushik Sen (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages396–411.

[Jaffar et al(2009)]
authorpersonJoxan Jaffar, personAndrew E. Santosa, and personRăzvan Voicu. year2009.
An Interpolation Method for CLP Traversal. In booktitlePrinciples and Practice of Constraint Programming - CP 2009, editorpersonIan P. Gent (Ed.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages454–469.

[Katz et al(2019)]
authorpersonGuy Katz, personDerek Huang, personDuligur Ibeling, personKyle Julian, personChristopher Lazarus, personRachel Lim, personParth Shah, personShantanu Thakoor, personHaoze Wu, personAleksandar Zeljić, personDavid Dill, personMykel Kochenderfer, and personClark Barrett. year2019.
booktitleThe Marabou Framework for Verification and Analysis of Deep Neural Networks.

[Keuchel et al(2022)]
authorpersonSteven Keuchel, personSander Huyghebaert, personGeorgy Lukyanov, and personDominique Devriese. year2022.
Verified Symbolic Execution with Kripke Specification Monads (and No Meta-Programming).
journalProc. ACM Program. Lang. volume6, numberICFP, Article articleno97 (dateaug year2022), numpages31 pages.

[Khanh and Ogawa(2012)]
authorpersonTo Van Khanh and personMizuhito Ogawa. year2012.
SMT for Polynomial Constraints on Real Numbers. In booktitleTAPAS@SAS.

[Khurshid et al(2003)]
authorpersonSarfraz Khurshid, personCorina S. PĂsĂreanu, and personWillem Visser. year2003.
Generalized Symbolic Execution for Model Checking and Testing. In booktitleTools and Algorithms for the Construction and Analysis of Systems, editorpersonHubert Garavel and personJohn Hatcliff (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages553–568.

[Li et al(2023)]
authorpersonLinyi Li, personTao Xie, and personBo Li. year2023.
SoK: Certified Robustness for Deep Neural Networks. In booktitle44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, 22-26 May 2023. publisherIEEE.

[Lin et al(2023)]
authorpersonZhengyao Lin, personXiaohong Chen, personMinh-Thai Trinh, personJohn Wang, and personGrigore Roşu. year2023.
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier.
journalProc. ACM Program. Lang. volume7, numberOOPSLA1, Article articleno77 (dateapr year2023), numpages29 pages.

[Lorenz et al(2021)]
authorpersonT. Lorenz, personA. Ruoss, personM. Balunovic, personG. Singh, and personM. Vechev. year2021.
Robustness Certification for Point Cloud Models. In booktitle2021 IEEE/CVF International Conference on Computer Vision (ICCV). publisherIEEE Computer Society, addressLos Alamitos, CA, USA, pages7588–7598.

[Lyu et al(2020)]
authorpersonZhaoyang Lyu, personChing-Yun Ko, personZhifeng Kong, personNgai Wong, personDahua Lin, and personLuca Daniel. year2020.
Fastened CROWN: Tightened Neural Network Robustness Certificates. In booktitleThe Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. publisherAAAI Press, pages5037–5044.

[Madry et al(2018)]
authorpersonAleksander Madry, personAleksandar Makelov, personLudwig Schmidt, personDimitris Tsipras, and personAdrian Vladu. year2018.
Towards Deep Learning Models Resistant to Adversarial Attacks. In booktitleInternational Conference on Learning Representations.

authorpersonKenneth L. McMillan. year2010.
Lazy Annotation for Program Testing and Verification. In booktitleComputer Aided Verification, editorpersonTayssir Touili, personByron Cook, and personPaul Jackson (Eds.). publisherSpringer Berlin Heidelberg, addressBerlin, Heidelberg, pages104–118.

[Müller et al(2021)]
authorpersonChristoph Müller, personFrançois Serre, personGagandeep Singh, personMarkus Püschel, and personMartin T. Vechev. year2021.
Scaling Polyhedral Neural Network Verification on GPUs. In booktitleProceedings of Machine Learning and Systems 2021, MLSys 2021, virtual, April 5-9, 2021, editorpersonAlex Smola, personAlex Dimakis, and personIon Stoica (Eds.). publishermlsys.org.

[Paszke et al(2019)]
authorpersonAdam Paszke, personSam Gross, personFrancisco Massa, personAdam Lerer, personJames Bradbury, personGregory Chanan, personTrevor Killeen, personZeming Lin, personNatalia Gimelshein, personLuca Antiga, personAlban Desmaison, personAndreas Köpf, personEdward Yang, personZach DeVito, personMartin Raison, personAlykhan Tejani, personSasank Chilamkurthy, personBenoit Steiner, personLu Fang, personJunjie Bai, and personSoumith Chintala. year2019.
booktitlePyTorch: An Imperative Style, High-Performance Deep Learning Library.
publisherCurran Associates Inc., addressRed Hook, NY, USA.

[Pham et al(2020)]
authorpersonLong H. Pham, personJiaying Li, and personJun Sun. year2020.
SOCRATES: Towards a Unified Platform for Neural Network Verification.
journalArXiv  volumeabs/2007.11206 (year2020).

[Raghunathan et al(2018)]
authorpersonAditi Raghunathan, personJacob Steinhardt, and personPercy Liang. year2018.
Semidefinite Relaxations for Certifying Robustness to Adversarial Examples. In booktitleProceedings of the 32nd International Conference on Neural Information Processing Systems (Montréal, Canada) (seriesNIPS'18). publisherCurran Associates Inc., addressRed Hook, NY, USA, pages10900–10910.

[Salman et al(2019)]
authorpersonHadi Salman, personGreg Yang, personHuan Zhang, personCho-Jui Hsieh, and personPengchuan Zhang. year2019.
booktitleA Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks.
publisherCurran Associates Inc., addressRed Hook, NY, USA.

[Scott et al(2022)]
authorpersonJoseph Scott, personGuanting Pan, personElias B. Khalil, and personVijay Ganesh. year2022.
Goose: A Meta-Solver for Deep Neural Network Verification. In booktitleProceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, August 11-12, 2022 (seriesCEUR Workshop Proceedings, Vol. volume3185), editorpersonDavid Déharbe and personAntti E. J. Hyvärinen (Eds.). publisherCEUR-WS.org, pages99–113.

[Sen et al(2005)]
authorpersonKoushik Sen, personDarko Marinov, and personGul Agha. year2005.
CUTE: A Concolic Unit Testing Engine for C. In booktitleProceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (Lisbon, Portugal) (seriesESEC/FSE-13). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages263–272.

[Shriver et al(2021)]
authorpersonDavid Shriver, personSebastian Elbaum, and personMatthew B. Dwyer. year2021.
DNNV: A Framework for Deep Neural Network Verification. In booktitleComputer Aided Verification, editorpersonAlexandra Silva and personK. Rustan M. Leino (Eds.). publisherSpringer International Publishing, addressCham, pages137–150.

[Si et al(2018)]
authorpersonXujie Si, personHanjun Dai, personMukund Raghothaman, personMayur Naik, and personLe Song. year2018.
Learning Loop Invariants for Program Verification. In booktitleAdvances in Neural Information Processing Systems, editorpersonS. Bengio, personH. Wallach, personH. Larochelle, personK. Grauman, personN. Cesa-Bianchi, and personR. Garnett (Eds.), Vol. volume31. publisherCurran Associates, Inc.

[Singh et al(2019a)]
authorpersonGagandeep Singh, personRupanshu Ganvir, personMarkus Püschel, and personMartin Vechev. year2019a.
booktitleBeyond the Single Neuron Convex Barrier for Neural Network Certification.
publisherCurran Associates Inc., addressRed Hook, NY, USA.

[Singh et al(2018a)]
authorpersonGagandeep Singh, personTimon Gehr, personMatthew Mirman, personMarkus Püschel, and personMartin Vechev. year2018a.
Fast and effective robustness certification.
journalAdvances in Neural Information Processing Systems  volume31 (year2018).

[Singh et al(2019b)]
authorpersonGagandeep Singh, personTimon Gehr, personMarkus Püschel, and personMartin Vechev. year2019b.
An abstract domain for certifying neural networks.
journalProceedings of the ACM on Programming Languages volume3, numberPOPL (year2019).

[Singh et al(2018b)]
authorpersonGagandeep Singh, personTimon Gehr, personMarkus Püschel, and personMartin T. Vechev. year2018b.
Boosting Robustness Certification of Neural Networks. In booktitleInternational Conference on Learning Representations.

[Singh et al(2018c)]
authorpersonGagandeep Singh, personTimon Gehr, personMarkus Püschel, and personMartin T. Vechev. year2018c.
titleETH Robustness Analyzer for Neural Networks (ERAN).

[Singh et al(2018d)]
authorpersonGagandeep Singh, personJingxuan He, personChristoph Müller, personFrançois Serre, personAnian Ruoss, personGleb Makarchuk, personMarkus Püschel, and personMartin T. Vechev. year2018d.
titleELINA: ETH LIbrary for Numerical Analysis.

[Singh et al(2017)]
authorpersonGagandeep Singh, personMarkus Püschel, and personMartin Vechev. year2017.
Fast Polyhedra Abstract Domain. In booktitleProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (seriesPOPL '17). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages46–59.

[Sotoudeh et al(2023)]
authorpersonMatthew Sotoudeh, personZhe Tao, and personAditya Thakur. year2023.
SyReNN: A tool for analyzing deep neural networks.
journalInternational Journal on Software Tools for Technology Transfer  volume25 (date02 year2023), pages1–21.

[Tjandraatmadja et al(2020)]
authorpersonChristian Tjandraatmadja, personRoss Anderson, personJoey Huchette, personWill Ma, personKrunal Patel, and personJuan Pablo Vielma. year2020.
The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification. In booktitleProceedings of the 34th International Conference on Neural Information Processing Systems (Vancouver, BC, Canada) (seriesNIPS'20). publisherCurran Associates Inc., addressRed Hook, NY, USA, Article articleno1819, numpages12 pages.

[Tjeng et al(2019)]
authorpersonVincent Tjeng, personKai Yuanqing Xiao, and personRuss Tedrake. year2019.
Evaluating Robustness of Neural Networks with Mixed Integer Programming. In booktitle7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. publisherOpenReview.net.

[Torlak and Bodik(2013)]
authorpersonEmina Torlak and personRastislav Bodik. year2013.
Growing Solver-Aided Languages with Rosette. In booktitleProceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Indianapolis, Indiana, USA) (seriesOnward! 2013). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages135–152.

[Torlak and Bodik(2014)]
authorpersonEmina Torlak and personRastislav Bodik. year2014.
A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages.
journalSIGPLAN Not. volume49, number6 (datejun year2014), pages530–541.

[Tran et al(2020)]
authorpersonHoang-Dung Tran, personStanley Bak, personWeiming Xiang, and personTaylor T. Johnson. year2020.
Verification of Deep Convolutional Neural Networks Using ImageStars. In booktitleComputer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I (Los Angeles, CA, USA). publisherSpringer-Verlag, addressBerlin, Heidelberg, pages18–42.

[Tran et al(2019)]
authorpersonHoang-Dung Tran, personDiago Manzanas Lopez, personPatrick Musau, personXiaodong Yang, personLuan Viet Nguyen, personWeiming Xiang, and personTaylor T. Johnson. year2019.
Star-Based Reachability Analysis of Deep Neural Networks. In booktitleFormal Methods – The Next 30 Years, editorpersonMaurice H. ter Beek, personAnnabelle McIver, and personJosé N. Oliveira (Eds.). publisherSpringer International Publishing, addressCham, pages670–686.

[Ugare et al(2023)]
authorpersonShubham Ugare, personDebangshu Banerjee, personSasa Misailovic, and personGagandeep Singh. year2023.
Incremental Verification of Neural Networks.
journalProc. ACM Program. Lang. volume7, numberPLDI, Article articleno185 (datejun year2023), numpages26 pages.

[Ugare et al(2022)]
authorpersonShubham Ugare, personGagandeep Singh, and personSasa Misailovic. year2022.
Proof transfer for fast certification of multiple approximate neural networks.
journalProc. ACM Program. Lang. volume6, numberOOPSLA1, Article articleno75 (dateapr year2022), numpages29 pages.

[Urban et al(2020)]
authorpersonCaterina Urban, personMaria Christakis, personValentin Wüstholz, and personFuyuan Zhang. year2020.
Perfectly Parallel Fairness Certification of Neural Networks.
journalProc. ACM Program. Lang. volume4, numberOOPSLA, Article articleno185 (datenov year2020), numpages30 pages.

[Vishwanathan et al(2023)]
authorpersonHarishankar Vishwanathan, personMatan Shachnai, personSrinivas Narayana, and personSantosh Nagarakatte. year2023.
Verifying the Verifier: eBPF Range Analysis Verification. In booktitleComputer Aided Verification.

[Visser et al(2004)]
authorpersonWillem Visser, personCorina S. Pundefinedsundefinedreanu, and personSarfraz Khurshid. year2004.
Test Input Generation with Java PathFinder. In booktitleProceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis (Boston, Massachusetts, USA) (seriesISSTA '04). publisherAssociation for Computing Machinery, addressNew York, NY, USA, pages97–107.

[Wang et al(2018a)]
authorpersonShiqi Wang, personKexin Pei, personJustin Whitehouse, personJunfeng Yang, and personSuman Jana. year2018a.
Efficient formal safety analysis of neural networks. In booktitleAdvances in Neural Information Processing Systems.

[Wang et al(2018b)]
authorpersonShiqi Wang, personKexin Pei, personJustin Whitehouse, personJunfeng Yang, and personSuman Jana. year2018b.
Formal Security Analysis of Neural Networks Using Symbolic Intervals. In booktitleProceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (seriesSEC'18). publisherUSENIX Association, addressUSA, pages1599–1614.

[Wang et al(2018c)]
authorpersonShiqi Wang, personKexin Pei, personJustin Whitehouse, personJunfeng Yang, and personSuman Jana. year2018c.
Formal Security Analysis of Neural Networks Using Symbolic Intervals. In booktitleProceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (seriesSEC'18). publisherUSENIX Association, addressUSA, pages1599–1614.

[Wang et al(2021)]
authorpersonShiqi Wang, personHuan Zhang, personKaidi Xu, personXue Lin, personSuman Jana, personCho-Jui Hsieh, and personJ Zico Kolter. year2021.
Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification.
journalarXiv preprint arXiv:2103.06624 (year2021).

[Weng et al(2018)]
authorpersonLily Weng, personHuan Zhang, personHongge Chen, personZhao Song, personCho-Jui Hsieh, personLuca Daniel, personDuane Boning, and personInderjit Dhillon. year2018.
Towards Fast Computation of Certified Robustness for ReLU Networks. In booktitleProceedings of the 35th International Conference on Machine Learning (seriesProceedings of Machine Learning Research, Vol. volume80), editorpersonJennifer Dy and personAndreas Krause (Eds.). publisherPMLR, pages5276–5285.

[Wong and Kolter(2018)]
authorpersonEric Wong and personJ. Zico Kolter. year2018.
Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In booktitleProceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, July 10-15, 2018 (seriesProceedings of Machine Learning Research, Vol. volume80), editorpersonJennifer G. Dy and personAndreas Krause (Eds.). publisherPMLR, pages5283–5292.

[Wu et al(2022)]
authorpersonHaoze Wu, personClark Barrett, personMahmood Sharif, personNina Narodytska, and personGagandeep Singh. year2022.
Scalable Verification of GNN-Based Job Schedulers.
journalProc. ACM Program. Lang. volume6, numberOOPSLA2, Article articleno162 (dateoct year2022), numpages30 pages.

[Wu et al(2020)]
authorpersonHaoze Wu, personAlex Ozdemir, personAleksandar Zeljić, personKyle Julian, personAhmed Irfan, personDivya Gopinath, personSadjad Fouladi, personGuy Katz, personCorina Pasareanu, and personClark Barrett. year2020.
Parallelization Techniques for Verifying Neural Networks. In booktitle2020 Formal Methods in Computer Aided Design (FMCAD). pages128–137.

[Xiang et al(2017)]
authorpersonWeiming Xiang, personHoang-Dung Tran, and personTaylor T. Johnson. year2017.
Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks.
journalCoRR  volumeabs/1708.03322 (year2017).

[Xu and Singh(2023)]
authorpersonChangming Xu and personGagandeep Singh. year2023.
titleRobust Universal Adversarial Perturbations.

[Xu et al(2020a)]
authorpersonKaidi Xu, personZhouxing Shi, personHuan Zhang, personYihan Wang, personKai-Wei Chang, personMinlie Huang, personBhavya Kailkhura, personXue Lin, and personCho-Jui Hsieh. year2020a.
Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond.

[Xu et al(2018)]
authorpersonKaidi Xu, personZhouxing Shi, personHuan Zhang, personYihan Wang, personKai-Wei Chang, personMinlie Huang, personBhavya Kailkhura, personXue Lin, and personCho-Jui Hsieh. year2018.
titleauto_LiRPA: An Automatic Linear Relaxation-based Perturbation Analysis Library for Neural Networks and General Computational Graphs.

[Xu et al(2020b)]
authorpersonKaidi Xu, personHuan Zhang, personShiqi Wang, personYihan Wang, personSuman Sekhar Jana, personXue Lin, and personCho-Jui Hsieh. year2020b.
Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers.
journalArXiv  volumeabs/2011.13824 (year2020).

[Yang et al(2021)]
authorpersonPengfei Yang, personRenjue Li, personJianlin Li, personCheng-Chao Huang, personJingyi Wang, personJun Sun, personBai Xue, and personLijun Zhang. year2021.
booktitleImproving Neural Network Verification through Spurious Region Guided Refinement.

[Zelazny et al(2022)]
authorpersonTom Zelazny, personHaoze Wu, personClark W. Barrett, and personGuy Katz. year2022.
On Optimizing Back-Substitution Methods for Neural Network Verification.
journal2022 Formal Methods in Computer-Aided Design (FMCAD) (year2022), pages17–26.

[Zhang et al(2018)]
authorpersonHuan Zhang, personTsui-Wei Weng, personPin-Yu Chen, personCho-Jui Hsieh, and personLuca Daniel. year2018.
Efficient Neural Network Robustness Certification with General Activation Functions. In booktitleProceedings of the 32nd International Conference on Neural Information Processing Systems (seriesNIPS'18). publisherCurran Associates Inc., addressRed Hook, NY, USA, pages4944–4953.