{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T18:14:18Z","timestamp":1771697658301,"version":"3.50.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2020,11]]},"DOI":"10.1007\/s11390-020-0546-7","type":"journal-article","created":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T11:11:43Z","timestamp":1607339503000},"page":"1365-1381","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Verifying ReLU Neural Networks from a Model Checking Perspective"],"prefix":"10.1007","volume":"35","author":[{"given":"Wan-Wei","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tang-Hao-Ran","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,11,30]]},"reference":[{"key":"546_CR1","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF02478259","volume":"5","author":"WS Mcculloch","year":"1943","unstructured":"Mcculloch W S, Pitts W. A logical calculus of the ideas immanent in nervous activity. Bulletin of Mathematical Biophysics, 1943, 5: 115-133.","journal-title":"Bulletin of Mathematical Biophysics"},{"key":"546_CR2","unstructured":"Salehinejad H, Baarbe J, Sankar S, Barfett J, Colak E, Valaee S. Recent advances in recurrent neural networks. arXiv:1801.01078, 2018. https:\/\/arxiv.org\/abs\/1801.01078, May 2020."},{"key":"546_CR3","unstructured":"LeCun Y. Generalization and network design strategies. In Connectionism in Perspective, Pfeifer R, Schreter Z, Fogelman-Souli\u00e9 F, Steels L (eds.), Elsevier, 1989, pp.143-155."},{"key":"546_CR4","unstructured":"Nair V, Hinton G E. Rectified linear units improve restricted Boltzmann machines. In Proc. the 27th International Conference on Machine Learning, June 2010, pp.807-814."},{"key":"546_CR5","unstructured":"Lei N, Luo Z, Yau S, Gu X D. Geometric understanding of deep learning. arXiv:1805.10451, 2018. https:\/\/arxiv.org\/abs\/1805.10451, May 2020."},{"key":"546_CR6","doi-asserted-by":"crossref","unstructured":"Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. the 3rd Workshop on Logics of Programs, May 1981, pp.52-71.","DOI":"10.1007\/BFb0025774"},{"key":"546_CR7","doi-asserted-by":"crossref","unstructured":"Queille J, Sifakis J. Specification and verification of concurrent systems in CESAR. In Proc. the 5th Int. Symp. Programming, April 1982, pp.337-351.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"546_CR8","doi-asserted-by":"crossref","unstructured":"Katz G, Barrett C W, Dill D L, Julian K, Kochenderfer M J. Reluplex: An efficient SMT solver for verifying deep neural networks. In Proc. the 29th Int. Conf. Computer Aided Verification, July 2017, pp.97-117.","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"546_CR9","doi-asserted-by":"crossref","unstructured":"Pnueli A. The temporal logic of programs. In Proc. the 18th Annual Symp. Foundations of Computer Science, October 1977, pp.46-57.","DOI":"10.1109\/SFCS.1977.32"},{"key":"546_CR10","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R. On the synthesis of a reactive module. In Proc. the 16th Annual ACM Symp. Principles of Programming Languages, January 1989, pp.179-190.","DOI":"10.1145\/75277.75293"},{"key":"546_CR11","doi-asserted-by":"crossref","unstructured":"Manna Z, Zarba C G. Combining decision procedures. In Proc. the 10th Anniversary Colloquium of the Int. Institute for Software Technology of the United Nations University, March 2002, pp.381-422.","DOI":"10.1007\/978-3-540-40007-3_24"},{"issue":"1\/2","key":"546_CR12","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport J H, Heintz J. Real quantifier elimination is doubly exponential. J. Symbolic Computation, 1988, 5(1\/2): 29-35.","journal-title":"J. Symbolic Computation"},{"key":"546_CR13","doi-asserted-by":"crossref","unstructured":"Huang X, Kwiatkowska M, Wang S, Wu M. Safety verification of deep neural networks. In Proc. the 29th Int. Conf. Computer Aided Verification, July 2017, pp.3-29.","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"546_CR14","doi-asserted-by":"crossref","unstructured":"Ruan W, Huang X, Kwiatkowska M. Reachability analysis of deep neural networks with provable guarantees. In Proc. the 27th Int. Joint Conf. Artificial Intelligence, July 2018, pp.2651-2659.","DOI":"10.24963\/ijcai.2018\/368"},{"key":"546_CR15","doi-asserted-by":"crossref","unstructured":"Pulina L, Tacchella A. An abstraction-refinement approach to verification of artificial neural networks. In Proc. the 22nd Int. Conf. Computer Aided Verification, July 2010, pp.243-257.","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"546_CR16","doi-asserted-by":"crossref","unstructured":"Dutta S, Jha S, Sankaranarayanan S, Tiwari A. Output range analysis for deep feedforward neural networks. In Proc. the 10th Int. Symposium NASA Formal Methods, April 2018, pp.121-138.","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"546_CR17","unstructured":"Weng T, Zhang H, Chen H, Song Z, Hsieh C, Daniel L, Duane S B, Dhillon I S. Towards fast computation of certified robustness for ReLU networks. In Proc. the 35th Int. Conf. Machine Learning, July 2018, pp.5273-5282."},{"key":"546_CR18","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1017\/S0305004100030401","volume":"51","author":"R Penrose","year":"1955","unstructured":"Penrose R. A generalized inverse for matrices. Mathematical Proc. the Cambridge, 1955, 51: 406-413.","journal-title":"Mathematical Proc. the Cambridge"},{"issue":"1","key":"546_CR19","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1017\/S0305004100030929","volume":"52","author":"R Penrose","year":"1956","unstructured":"Penrose R. On the best approximate solution of linear matrix equations. Mathematical Proceedings of the Cambridge Philosophical Society, 1956, 52(1): 17-19.","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"546_CR20","doi-asserted-by":"crossref","unstructured":"Farkas G. \u00fcber die theorie der einfachen ungleichungen. J. die Reine und Angewandte Mathematik, 1902, 124: 1-24. (in German)","DOI":"10.1515\/crll.1902.124.1"},{"key":"546_CR21","unstructured":"Lomuscio A, Maganti L. An approach to reachability analysis for feed-forward ReLU neural networks. arXiv:1706.07351, 2017. https:\/\/arxiv.org\/abs\/1706.07351, May 2020."},{"key":"546_CR22","unstructured":"Huang X, Kroening D, Ruan W, Sharp J, Sun Y, Thamo E, Wu M, Yi X. Safety and trustworthiness of deep neural networks: A survey. arXiv:1812.08342v4, 2019. https:\/\/arxiv.org\/abs\/1812.08342, April 2020."},{"key":"546_CR23","unstructured":"Szegedy C, Zaremba W, Sutskever I, Bruna J, Erhan D, Goodfellow I J, Fergus R. Intriguing properties of neural networks. In Proc. the 2nd Int. Conf. Learning Representations, April 2014."},{"key":"546_CR24","unstructured":"Lei Y, Chen S, Fan L, Song F, Liu Y. Advanced evasion attacks and mitigations on practical ML-based phishing website classifiers. arXiv:2004.06954, 2020. https:\/\/arxiv.org\/abs\/2004.06954, May 2020."},{"key":"546_CR25","unstructured":"Chen G, Chen S, Fan L, Du X, Zhao Z, Song F, Liu Y. Who is real Bob? Adversarial attacks on speaker recognition systems. arXiv:1911.01840, 2019. https:\/\/arxiv.org\/abs\/1911.01840, May 2020."},{"key":"546_CR26","unstructured":"Duan Y, Zhao Z, Bu L, Song F. Things you may not know about adversarial example: A black-box adversarial image attack. arXiv:1905.07672, 2019. https:\/\/arxiv.org\/abs\/1905.07672, May 2020."},{"key":"546_CR27","doi-asserted-by":"crossref","unstructured":"Narodytska N, Kasiviswanathan S P, Ryzhyk L, Sagiv M, Walsh T. Verifying properties of binarized deep neural networks. In Proc. the 32nd AAAI Conf. Artificial Intelligence, February 2018, pp.6615-6624.","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"546_CR28","doi-asserted-by":"crossref","unstructured":"Cheng C, N\u00fchrenberg G, Ruess H. Maximum resilience of artificial neural networks. In Proc. the 15th Int. Symp. Automated Technology for Verification and Analysis, October 2017, pp.251-268.","DOI":"10.1007\/978-3-319-68167-2_18"},{"key":"546_CR29","unstructured":"Bunel R, Turkaslan I, Torr P H S, Kohli P, Mudigonda P K. A unified view of piecewise linear neural network verification. In Proc. the 32nd Annual Conf. Neural Information Processing Systems, December 2018, pp.4795-4804."},{"key":"546_CR30","doi-asserted-by":"crossref","unstructured":"Tran H, Lopez D M, Musau P, Yang X, Nguyen L V, Xiang W, Johnson T T. Star-based reachability analysis of deep neural networks. In Proc. the 3rd World Congress on Formal Methods, October 2019, pp.670-686.","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"546_CR31","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. the 4th ACM Symp. Principles of Programming Languages, January 1977, pp.238-252.","DOI":"10.1145\/512950.512973"},{"key":"546_CR32","doi-asserted-by":"crossref","unstructured":"Gehr T, Mirman M, Drachsler-Cohen D, Tsankov P, Chaudhuri S, Vechev M T. AI2: Safety and robustness certification of neural networks with abstract interpretation. In Proc. the 39th IEEE Symp. Security and Privacy, May 2018, pp.3-18.","DOI":"10.1109\/SP.2018.00058"},{"key":"546_CR33","unstructured":"Wang S, Pei K, Whitehouse J, Yang J, Jana S. Formal security analysis of neural networks using symbolic intervals. In Proc. the 27th USENIX Security Symp., August 2018, pp.1599-1614."},{"key":"546_CR34","unstructured":"Singh G, Gehr T, P\u00fcschel M, Vechev M. T. Boosting robustness certification of neural networks. In Proc.the 7th International Conference on Learning Representations, May 2019."},{"key":"546_CR35","unstructured":"Wan W, Zhang Z, Zhu Y, Zhang M, Song F. Accelerating robustness verification of deep neural networks guided by target labels. arXiv:2007.08520, 2020. https:\/\/arxiv.org\/abs\/2007.08520, July 2020."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-020-0546-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-020-0546-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-020-0546-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,3]],"date-time":"2022-12-03T00:04:20Z","timestamp":1670025860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-020-0546-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11]]},"references-count":35,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["546"],"URL":"https:\/\/doi.org\/10.1007\/s11390-020-0546-7","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11]]},"assertion":[{"value":"12 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 October 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 November 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}