{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T06:45:48Z","timestamp":1773384348979,"version":"3.50.1"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319779348","type":"print"},{"value":"9783319779355","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-77935-5_9","type":"book-chapter","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T15:02:34Z","timestamp":1520694154000},"page":"121-138","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":184,"title":["Output Range Analysis for Deep Feedforward Neural Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2706-2095","authenticated-orcid":false,"given":"Souradeep","family":"Dutta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5983-9095","authenticated-orcid":false,"given":"Susmit","family":"Jha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7315-4340","authenticated-orcid":false,"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5153-2686","authenticated-orcid":false,"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,11]]},"reference":[{"key":"9_CR1","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"9_CR2","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. Handb. Satisfiability 185, 825\u2013885 (2009)"},{"key":"9_CR3","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., Criminisi, A.: Measuring neural net robustness with constraints. In: Advances in Neural Information Processing Systems, pp. 2613\u20132621 (2016)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Bixby, R.E.: A brief history of linear and mixed-integer programming computation. Documenta Mathematica 107\u2013121 (2012)","DOI":"10.4171\/dms\/6\/16"},{"key":"9_CR5","unstructured":"Bunel, R., Turkaslan, I., Torr, P.H.S., Kohli, P., Kumar, M.P.: Piecewise linear neural network verification: a comparative study. CoRR, abs\/1711.00455 (2017)"},{"key":"9_CR6","unstructured":"Dutta, S.: Sherlock: an output range analysis tool for neural networks. https:\/\/github.com\/souradeep-111\/sherlock"},{"key":"9_CR7","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Verified inference of feedback control systems using feedforward neural networks. Draft (2017). Available upon request"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269\u2013286. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_19","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"9_CR9","unstructured":"Gurobi Optimization, Inc.: Gurobi optimizer reference manual (2016)"},{"key":"9_CR10","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. CoRR, abs\/1610.06940 (2016)"},{"key":"9_CR11","unstructured":"IBM ILOG Inc.: CPLEX MILP Solver (1992)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Julian, K., Kochenderfer, M.J.: Neural network guidance for UAVs. In: AIAA Guidance Navigation and Control Conference (GNC) (2017)","DOI":"10.2514\/6.2017-1743"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Kahn, G., Zhang, T., Levine, S., Abbeel, P.: Plato: policy learning using adaptive trajectory optimization. arXiv preprint arXiv:1603.00622 (2016)","DOI":"10.1109\/ICRA.2017.7989379"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"9_CR15","unstructured":"Katz, et al.: Reluplex: CAV 2017 prototype (2017). https:\/\/github.com\/guykatzz\/ReluplexCav2017"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-540-45224-9_24","volume-title":"Knowledge-Based Intelligent Information and Engineering Systems","author":"Z Kurd","year":"2003","unstructured":"Kurd, Z., Kelly, T.: Establishing safety criteria for artificial neural networks. In: Palade, V., Howlett, R.J., Jain, L. (eds.) KES 2003. LNCS (LNAI), vol. 2773, pp. 163\u2013169. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45224-9_24"},{"issue":"7553","key":"9_CR17","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1038\/nature14539","volume":"521","author":"Y LeCun","year":"2015","unstructured":"LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521(7553), 436\u2013444 (2015)","journal-title":"Nature"},{"key":"9_CR18","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. CoRR, abs\/1706.07351 (2017)"},{"key":"9_CR19","unstructured":"Luenberger, D.G.: Optimization by Vector Space Methods. Wiley, Hoboken (1969)"},{"key":"9_CR20","unstructured":"Mitchell, J.E.: Branch-and-cut algorithms for combinatorial optimization problems. In: Handbook of Applied Optimization, pp. 65\u201377 (2002)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P.D., Goodfellow, I.J., Jha, S., Celik, Z.B., Swami, A.: Practical black-box attacks against deep learning systems using adversarial examples. CoRR, abs\/1602.02697 (2016)","DOI":"10.1145\/3052973.3053009"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14295-6_24","volume-title":"Computer Aided Verification","author":"L Pulina","year":"2010","unstructured":"Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 243\u2013257. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_24"},{"issue":"2","key":"9_CR23","doi-asserted-by":"crossref","first-page":"117","DOI":"10.3233\/AIC-2012-0525","volume":"25","author":"L Pulina","year":"2012","unstructured":"Pulina, L., Tacchella, A.: Challenging SMT solvers to verify neural networks. AI Commun. 25(2), 117\u2013135 (2012)","journal-title":"AI Commun."},{"key":"9_CR24","unstructured":"Sassi, M.A.B., Bartocci, E., Sankaranarayanan, S.: A linear programming-based iterative approach to stabilizing polynomial dynamics. In: Proceedings of IFAC 2017. Elsevier, Amsterdam (2017)"},{"key":"9_CR25","unstructured":"Scheibler, K., Winterer, L., Wimmer, R., Becker, B.: Towards verification of artificial neural networks. In: MBMV Workshop, pp. 30\u201340 (2015)"},{"key":"9_CR26","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks. CoRR, abs\/1312.6199 (2013)"},{"key":"9_CR27","unstructured":"Tjeng, V., Tedrake, R.: Verifying neural networks with mixed integer programming. CoRR, abs\/1711.07356 (2017)"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Vanderbei, R.J.: Linear Programming: Foundations & Extensions, Second edn. Springer, Heidelberg (2001). Cf. http:\/\/www.princeton.edu\/~rvdb\/LPbook\/","DOI":"10.1007\/978-1-4757-5662-3"},{"key":"9_CR29","volume-title":"Model Building in Mathematical Programming","author":"HP Williams","year":"2013","unstructured":"Williams, H.P.: Model Building in Mathematical Programming, 5th edn. Wiley, Hoboken (2013)","edition":"5"},{"key":"9_CR30","unstructured":"Xiang, W., Tran, H.-D., Johnson, T.T.: Output reachable set estimation and verification for multi-layer neural networks. CoRR, abs\/1708.03322 (2017)"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Xiang, W., Tran, H.-D., Rosenfeld, J.A., Johnson, T.T.: Reachable set estimation and verification for a class of piecewise linear systems with neural network controllers (2018). To Appear in the American Control Conference (ACC), Invited Session on Formal Methods in Controller Synthesis","DOI":"10.23919\/ACC.2018.8431048"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77935-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T15:06:58Z","timestamp":1693580818000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77935-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319779348","9783319779355"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77935-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}