{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:58:27Z","timestamp":1779087507483,"version":"3.51.4"},"reference-count":75,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T00:00:00Z","timestamp":1625097600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T00:00:00Z","timestamp":1625097600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","award":["N\/A"],"award-info":[{"award-number":["N\/A"]}],"id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,2]]},"DOI":"10.1007\/s10703-021-00363-7","type":"journal-article","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T16:09:35Z","timestamp":1625155775000},"page":"87-116","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Reluplex: a calculus for reasoning about deep neural networks"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7729-8373","authenticated-orcid":false,"given":"Guy","family":"Katz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kyle","family":"Julian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mykel J.","family":"Kochenderfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,1]]},"reference":[{"key":"363_CR1","doi-asserted-by":"crossref","unstructured":"Amir G, Wu H, Barrett C, Katz G (2020) An SMT-based approach for verifying binarized neural networks. Technical Report. arXiv:2011.02948","DOI":"10.26226\/morressier.604907f41a80aac83ca25cda"},{"key":"363_CR2","doi-asserted-by":"crossref","unstructured":"Barrett C, Nieuwenhuis R, Oliveras A, Tinelli C (2006) Splitting on demand in SAT modulo theories. In: Proceedings of 13th international conference on logic for programming, artificial intelligence, and reasoning (LPAR), pp 512\u2013526","DOI":"10.1007\/11916277_35"},{"key":"363_CR3","first-page":"825","volume-title":"Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications, chapter\u00a026","author":"C Barrett","year":"2009","unstructured":"Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories. In: Biere A, Heule MJH, van Maaren H, Walsh T (eds) Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications, chapter\u00a026, vol 185. IOS Press, New York, pp 825\u2013885"},{"key":"363_CR4","unstructured":"Bastani O, Ioannou Y, Lampropoulos L, Vytiniotis D, Nori A, Criminisi A (2016) Measuring neural net robustness with constraints. In: Proceedings of 30th conference on neural information processing systems (NIPS)"},{"key":"363_CR5","unstructured":"Bastani O, Pu Y, Solar-Lezama A (2018) Verifiable reinforcement learning via policy extraction. In: Proceedings of 32nd conference on neural information processing systems (NeurIPS)"},{"key":"363_CR6","unstructured":"Bojarski M, Del\u00a0Testa D, Dworakowski D, Firner B, Flepp B, Goyal P, Jackel L, Monfort M, Muller U, Zhang J, Zhang X, Zhao J, Zieba K (2016) End to end learning for self-driving cars. Technical Report. arXiv:1604.07316"},{"key":"363_CR7","unstructured":"Bunel R, Turkaslan I, Torr P, Kohli P, Kumar M (2017) Piecewise linear neural network verification: a comparative study. Technical Report. arXiv:1711.00455v1"},{"key":"363_CR8","unstructured":"Carlini N, Katz G, Barrett C, Dill D (2017) Provably Minimally-distorted adversarial examples. Technical Report. arXiv:1709.10207"},{"key":"363_CR9","unstructured":"Choi A, \u00a0Shi W, \u00a0Shih A, \u00a0Darwiche A (2019) Compiling neural networks into tractable boolean circuits. In: Proceedings of 1st AAAI spring symposium on verification of neural networks (VNN)"},{"key":"363_CR10","doi-asserted-by":"publisher","DOI":"10.7249\/R366","volume-title":"Linear programming and extensions","author":"G Dantzig","year":"1963","unstructured":"Dantzig G (1963) Linear programming and extensions. Princeton University Press, Princeton"},{"key":"363_CR11","doi-asserted-by":"crossref","unstructured":"Dutertre B, de\u00a0Moura L (2006) A fast linear-arithmetic solver for DPLL(T). In: Proceedings of 18th international conference on computer aided verification (CAV), pp 81\u201394","DOI":"10.1007\/11817963_11"},{"key":"363_CR12","doi-asserted-by":"crossref","unstructured":"Dutta S, Chen X, Sankaranarayanan S (2019) Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: Proceedings of 22nd ACM international conference on hybrid systems: computation and control (HSCC)","DOI":"10.1145\/3302504.3311807"},{"key":"363_CR13","doi-asserted-by":"crossref","unstructured":"Dutta S, Jha S, Sanakaranarayanan S, Tiwari A (2018) Output range analysis for deep neural networks. In: Proceedings of 10th NASA formal methods symposium (NFM), pp 121\u2013138","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"363_CR14","unstructured":"Dvijotham K, Stanforth R, Gowal S, Mann T, Kohli P (2018) A dual approach to scalable verification of deep networks. In: Proceedings of conference on uncertainty in artificial intelligence (UAI), pp 550\u2013559"},{"key":"363_CR15","doi-asserted-by":"crossref","unstructured":"Ehlers R (2017) Formal verification of piece-wise linear feed-forward neural networks. In: Proceedings of 15th international symposium on automated technology for verification and analysis (ATVA), pp 269\u2013286","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"363_CR16","doi-asserted-by":"crossref","unstructured":"Elboher Y, Gottschlich J, Katz G (2020) An abstraction-based framework for neural network verification. In: Proceedings of 32nd international conference on computer aided verification (CAV), pp 43\u201365","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"363_CR17","doi-asserted-by":"crossref","unstructured":"Faure G, Nieuwenhuis R, Oliveras A, Rodr\u00edguez-Carbonell E (2008) SAT modulo the theory of linear arithmetic: exact, inexact and commercial solvers. In: Proceedings of 11th international conference on theory and applications of satisfiability testing (SAT), pp 77\u201390","DOI":"10.1007\/978-3-540-79719-7_8"},{"key":"363_CR18","doi-asserted-by":"crossref","unstructured":"Gehr T, Mirman M, Drachsler-Cohen D, Tsankov E, Chaudhuri S, Vechev M (2018) AI2: safety and robustness certification of neural networks with abstract interpretation. In: Proceedings of 39th IEEE symposium on security and privacy (S&P)","DOI":"10.1109\/SP.2018.00058"},{"key":"363_CR19","unstructured":"Glorot X, Bordes A, Bengio Y (2011) Deep sparse rectifier neural networks. In: Proceedings of 14th international conference on artificial intelligence and statistics (AISTATS), pp 315\u2013323"},{"key":"363_CR20","doi-asserted-by":"crossref","unstructured":"Gokulanathan S, Feldsher A, Malca A, Barrett C, Katz G (2020) Simplifying neural networks using formal verification. In: Proceedings of 12th NASA formal methods symposium (NFM), pp 85\u201393","DOI":"10.1007\/978-3-030-55754-6_5"},{"key":"363_CR21","unstructured":"Goldberger B, Adi Y, Keshet J, Katz G (2020) Minimal modifications of deep neural networks using verification. In: Proceedings of 23rd international conference on logic for programming, artificial intelligence and reasoning (LPAR), pp 260\u2013278"},{"key":"363_CR22","volume-title":"Deep learning","author":"I Goodfellow","year":"2016","unstructured":"Goodfellow I, Bengio Y, Courville A (2016) Deep learning. MIT Press, Cambridge"},{"key":"363_CR23","unstructured":"Goodfellow I, Shlens J, Szegedy C (2014) Explaining and harnessing adversarial examples. Technical Report. arXiv:1412.6572"},{"key":"363_CR24","doi-asserted-by":"crossref","unstructured":"Gopinath D, Katz G, P\u01ces\u01cereanu C, Barrett C (2018) DeepSafe: a data-driven approach for assessing robustness of neural networks. In: Proceedings of 16th international symposium on automated technology for verification and analysis (ATVA), pp 3\u201319","DOI":"10.1007\/978-3-030-01090-4_1"},{"key":"363_CR25","unstructured":"Gowal S, Dvijotham K, Stanforth R, Bunel R, Qin C, Uesato J, Mann T, Kohli P (2018) On the effectiveness of interval bound propagation for training verifiably robust models. Technical Report. arXiv:1810.12715"},{"issue":"6","key":"363_CR26","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/MSP.2012.2205597","volume":"29","author":"G Hinton","year":"2012","unstructured":"Hinton G, Deng L, Yu D, Dahl G, Mohamed A, Jaitly N, Senior A, Vanhoucke V, Nguyen P, Sainath T, Kingsbury B (2012) Deep neural networks for acoustic modeling in speech recognition: the shared views of four research groups. IEEE Signal Process Mag 29(6):82\u201397","journal-title":"IEEE Signal Process Mag"},{"key":"363_CR27","doi-asserted-by":"crossref","unstructured":"Huang X, Kwiatkowska M, Wang S, Wu M (2016) Safety verification of deep neural networks. Technical Report. arXiv:1610.06940","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"363_CR28","doi-asserted-by":"crossref","unstructured":"Ivanov R, Weimer J, Alur R, Pappas G, Lee I (2019) Verisig: verifying safety properties of hybrid systems with neural network controllers. In: Proceedings of 22nd ACM international conference on hybrid systems: computation and control (HSCC)","DOI":"10.1145\/3302504.3311806"},{"key":"363_CR29","doi-asserted-by":"crossref","unstructured":"Jacoby Y, Barrett C, Katz G (2020) Verifying recurrent neural networks using invariant inference. In: Proceedings of 18th international symposium on automated technology for verification and analysis (ATVA), pp 57\u201374","DOI":"10.1007\/978-3-030-59152-6_3"},{"key":"363_CR30","doi-asserted-by":"crossref","unstructured":"Jarrett K, Kavukcuoglu K, LeCun Y (2009) What is the best multi-stage architecture for object recognition? In: Proceedings of 12th IEEE international conference on computer vision (ICCV), pp 2146\u20132153","DOI":"10.1109\/ICCV.2009.5459469"},{"key":"363_CR31","unstructured":"Jha S (2019) Logic extraction for explainable AI. In: Proceedings of 2nd workshop on formal methods for ML-enabled autonomous systems (FoMLAS)"},{"issue":"3","key":"363_CR32","doi-asserted-by":"publisher","first-page":"598","DOI":"10.2514\/1.G003724","volume":"42","author":"K Julian","year":"2019","unstructured":"Julian K, Kochenderfer M, Owen M (2019) Deep neural network compression for aircraft collision avoidance systems. J Guid Control Dyn 42(3):598\u2013608","journal-title":"J Guid Control Dyn"},{"key":"363_CR33","unstructured":"Katz G, Barrett C, Dill D, Julian K, Kochenderfer M (2017) Reluplex. https:\/\/github.com\/guykatzz\/ReluplexCav2017"},{"key":"363_CR34","doi-asserted-by":"crossref","unstructured":"Katz G, Barrett C, Dill D, Julian K, Kochenderfer M (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. In: Proceedings of 29th international conference on computer aided verification (CAV), pp 97\u2013117","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"363_CR35","doi-asserted-by":"crossref","unstructured":"Katz G, Barrett C, Dill D, Julian K, Kochenderfer M (2017) Towards proving the adversarial robustness of deep neural networks. In: Proceedings of 1st workshop on formal verification of autonomous vehicles (FVAV), pp 19\u201326","DOI":"10.4204\/EPTCS.257.3"},{"key":"363_CR36","doi-asserted-by":"crossref","unstructured":"Katz G, Barrett C, Tinelli C, Reynolds A, Hadarean L (2016) Lazy proofs for DPLL(T)-based SMT solvers. In: Proceedings of 16th international conference on formal methods in computer-aided design (FMCAD), pp 93\u2013100","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"363_CR37","doi-asserted-by":"crossref","unstructured":"Katz G, Huang D, Ibeling D, Julian K, Lazarus C, Lim R, Shah P, Thakoor S, Wu H, Zelji\u0107 A, Dill D, Kochenderfer M, Barrett C (2019) The Marabou framework for verification and analysis of deep neural networks. In: Proceedings of 31st international conference on computer aided verification (CAV), pp 443\u2013452","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"363_CR38","doi-asserted-by":"crossref","unstructured":"Kazak Y, Barrett C, Katz G, Schapira M (2019) Verifying deep-RL-driven systems. In: Proceedings of 1st ACM SIGCOMM workshop on network meets AI and ML (NetAI), pp 83\u201389","DOI":"10.1145\/3341216.3342218"},{"key":"363_CR39","unstructured":"King T (2014) Effective algorithms for the satisfiability of quantifier-free formulas over linear real and integer arithmetic. PhD Thesis"},{"key":"363_CR40","doi-asserted-by":"crossref","unstructured":"King T, Barret C, Tinelli C (2014) Leveraging linear and mixed integer programming for SMT. In: Proceedings of 14th international conference on formal methods in computer-aided design (FMCAD), pp 139\u2013146","DOI":"10.1109\/FMCAD.2014.6987606"},{"key":"363_CR41","doi-asserted-by":"crossref","unstructured":"Kochenderfer M (2015) Decision making under uncertainty: theory and application. In: Optimized airborne collision avoidance, chapter. MIT, pp 259\u2013276","DOI":"10.7551\/mitpress\/10187.001.0001"},{"key":"363_CR42","unstructured":"Kochenderfer M, Chryssanthacopoulos J (2011) Robust airborne collision avoidance through dynamic programming. Project Report ATC-371, Massachusetts Institute of Technology, Lincoln Laboratory"},{"issue":"2","key":"363_CR43","doi-asserted-by":"publisher","first-page":"487","DOI":"10.2514\/1.44867","volume":"33","author":"M Kochenderfer","year":"2010","unstructured":"Kochenderfer M, Edwards M, Espindle L, Kuchar J, Griffith J (2010) Airspace encounter models for estimating collision risk. AIAA J Guid Control Dyn 33(2):487\u2013499","journal-title":"AIAA J Guid Control Dyn"},{"issue":"1","key":"363_CR44","first-page":"17","volume":"19","author":"M Kochenderfer","year":"2012","unstructured":"Kochenderfer M, Holland J, Chryssanthacopoulos J (2012) Next generation airborne collision avoidance system. Lincoln Lab J 19(1):17\u201333","journal-title":"Lincoln Lab J"},{"key":"363_CR45","unstructured":"Kolter J, Wong E (2018) Provable defenses against adversarial examples via the convex outer adversarial polytope. In: Proceedings of 16th IEEE international conference on machine learning and applications (ICML)"},{"key":"363_CR46","unstructured":"Krizhevsky A, Sutskever I, Hinton G (2012) Imagenet classification with deep convolutional neural networks. In: Advances in neural information processing systems, pp 1097\u20131105"},{"issue":"2","key":"363_CR47","first-page":"277","volume":"16","author":"J Kuchar","year":"2007","unstructured":"Kuchar J, Drumm A (2007) The traffic alert and collision avoidance system. Lincoln Lab J 16(2):277\u2013296","journal-title":"Lincoln Lab J"},{"key":"363_CR48","unstructured":"Kuper L, Katz G, Gottschlich J, Julian K, Barrett C, Kochenderfer M (2018) Toward scalable verification for safety-critical deep networks. Technical Report. arXiv:1801.05950"},{"key":"363_CR49","unstructured":"Lin X, Zhu H, Samanta R, Jagannathan S (2019) ART: abstraction refinement-guided training for provably correct neural networks. Technical Report. arXiv:1907.10662"},{"key":"363_CR50","doi-asserted-by":"crossref","unstructured":"Liu C, Arnon T, Lazarus C, Strong C, Barrett C, Kochenderfer M (2020) Algorithms for verifying deep neural networks. Found Trends Optim 4","DOI":"10.1561\/9781680837872"},{"key":"363_CR51","unstructured":"Lomuscio A, Maganti L(2017) An approach to reachability analysis for feed-forward ReLU neural networks. Technical Report. arXiv:1706.07351"},{"key":"363_CR52","unstructured":"Maas A, Hannun A, Ng A (2013) Rectifier nonlinearities improve neural network acoustic models. In: Proceedings of 30th international conference on machine learning (ICML)"},{"issue":"5","key":"363_CR53","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J Marques-Silva","year":"1999","unstructured":"Marques-Silva J, Sakallah K (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506\u2013521","journal-title":"IEEE Trans Comput"},{"key":"363_CR54","unstructured":"Matthias H, Andriushchenko M (2017) Formal guarantees on the robustness of a classifier against adversarial manipulation. In: Proceedings of 31st conference on neural information processing systems (NeurIPS)"},{"key":"363_CR55","doi-asserted-by":"crossref","unstructured":"Monniaux D (2009) On using floating-point computations to help an exact linear arithmetic decision procedure. In: Proceedings of 21st international conference on computer aided verification (CAV), pp 570\u2013583","DOI":"10.1007\/978-3-642-02658-4_42"},{"key":"363_CR56","unstructured":"Nair V, Hinton G (2010) Rectified linear units improve restricted Boltzmann machines. In: Proceedings of 27th international conference on machine learning (ICML), pp 807\u2013814"},{"issue":"6","key":"363_CR57","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J ACM (JACM) 53(6):937\u2013977","journal-title":"J ACM (JACM)"},{"issue":"1","key":"363_CR58","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1137\/1033004","volume":"33","author":"M Padberg","year":"1991","unstructured":"Padberg M, Rinaldi G (1991) A branch-and-cut algorithm for the resolution of large-scale symmetric traveling salesman problems. SIAM Rev 33(1):60\u2013100","journal-title":"SIAM Rev"},{"key":"363_CR59","doi-asserted-by":"crossref","unstructured":"Pulina L, Tacchella A (2010) An abstraction-refinement approach to verification of artificial neural networks. In: Proceedings of 22nd international conference on computer aided verification (CAV), pp 243\u2013257","DOI":"10.1007\/978-3-642-14295-6_24"},{"issue":"2","key":"363_CR60","doi-asserted-by":"publisher","first-page":"117","DOI":"10.3233\/AIC-2012-0525","volume":"25","author":"L Pulina","year":"2012","unstructured":"Pulina L, Tacchella A (2012) Challenging SMT solvers to verify neural networks. AI Commun 25(2):117\u2013135","journal-title":"AI Commun"},{"key":"363_CR61","unstructured":"Raghunathan A, Steinhardt J, Liang P (2018) Certified defenses against adversarial examples. In: Proceedings of 6th international conference on learning representations (ICLR)"},{"issue":"11","key":"363_CR62","doi-asserted-by":"publisher","first-page":"1019","DOI":"10.1038\/14819","volume":"2","author":"M Riesenhuber","year":"1999","unstructured":"Riesenhuber M, Tomaso P (1999) Hierarchical models of object recognition in cortex. Nat Neurosci 2(11):1019\u20131025","journal-title":"Nat Neurosci"},{"key":"363_CR63","doi-asserted-by":"crossref","unstructured":"Ruan W, Huang X, Kwiatkowska M (2018) Reachability analysis of deep neural networks with provable guarantees. In: Proceedings of 27th international joint conference on artificial intelligence (IJCAI)","DOI":"10.24963\/ijcai.2018\/368"},{"issue":"7587","key":"363_CR64","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver D, Huang A, Maddison C, Guez A, Sifre L, Van Den Driessche G, Schrittwieser J, Antonoglou I, Panneershelvam V, Lanctot M, Dieleman S (2016) Mastering the game of go with deep neural networks and tree search. Nature 529(7587):484\u2013489","journal-title":"Nature"},{"key":"363_CR65","unstructured":"Singh G, Gehr T, Mirman M, Puschel M, Vechev M (2018) Fast and effective robustness certification. In: Proceedings of 32nd conference on neural information processing systems (NeurIPS)"},{"key":"363_CR66","doi-asserted-by":"crossref","unstructured":"Singh G, Gehr T, Puschel M, Vechev M (2019) An abstract domain for certifying neural networks. In: Proceedings of 6th ACM SIGPLAN symposium on principles of programming languages (POPL)","DOI":"10.1145\/3290354"},{"key":"363_CR67","doi-asserted-by":"crossref","unstructured":"Strong C, Wu H, Zelji\u0107 A, Julian K, Katz G, Barrett C, Kochenderfer M (2020) Global optimization of objective functions represented by ReLU networks. Technical Report. arXiv:2010.03258","DOI":"10.1007\/s10994-021-06050-2"},{"key":"363_CR68","doi-asserted-by":"crossref","unstructured":"Sun X, K H, Shoukry Y (2019) Formal verification of neural network controlled autonomous systems. In: Proceedings of 22nd ACM international conference on hybrid systems: computation and control (HSCC)","DOI":"10.1145\/3302504.3311802"},{"key":"363_CR69","unstructured":"Szegedy C, Zaremba W, Sutskever I, Bruna J, Erhan D, Goodfellow I, Fergus R (2013) Intriguing properties of neural networks. Technical Report. arXiv:1312.6199"},{"key":"363_CR70","unstructured":"Tjeng V, Xiao K, Tedrake R (2017) Evaluating robustness of neural networks with mixed integer programming. Technical Report. arXiv:1711.07356"},{"key":"363_CR71","volume-title":"Linear programming: foundations and extensions","author":"R Vanderbei","year":"1996","unstructured":"Vanderbei R (1996) Linear programming: foundations and extensions. Springer, Berlin"},{"key":"363_CR72","unstructured":"Wang S, Pei K, Whitehouse J, Yang J, Jana S (2018) Formal security analysis of neural networks using symbolic intervals. In: Proceedings of 27th USENIX security symposium"},{"key":"363_CR73","unstructured":"Wu H, Ozdemir A, Zelji\u0107 A, Irfan A, Julian K, Gopinath D, Fouladi S, Katz G, P\u0103s\u0103reanu C, Barrett C (2020) Parallelization techniques for verifying neural networks. In: Proceedings of 20th international conference on formal methods in computer-aided design (FMCAD), pp 128\u2013137"},{"key":"363_CR74","unstructured":"Xiang W, Johnson T (2018) Reachability analysis and safety verification for neural network control systems. Technical Report. arXiv:1805.09944"},{"key":"363_CR75","first-page":"1","volume":"99","author":"W Xiang","year":"2018","unstructured":"Xiang W, Tran H-D, Johnson T (2018) Output reachable set estimation and verification for multilayer neural networks. IEEE Trans Neural Netw Learn Syst (TNNLS) 99:1\u20137","journal-title":"IEEE Trans Neural Netw Learn Syst (TNNLS)"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00363-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00363-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00363-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T17:31:03Z","timestamp":1675877463000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00363-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,1]]},"references-count":75,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["363"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00363-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,1]]},"assertion":[{"value":"10 September 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 February 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 July 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}