{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,28]],"date-time":"2026-08-28T16:57:59Z","timestamp":1787936279943,"version":"build-2784847793"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319681665","type":"print"},{"value":"9783319681672","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_19","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"269-286","source":"Crossref","is-referenced-by-count":355,"title":["Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks"],"prefix":"10.1007","author":[{"given":"R\u00fcdiger","family":"Ehlers","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/j.neunet.2014.09.003","volume":"61","author":"J Schmidhuber","year":"2015","unstructured":"Schmidhuber, J.: Deep learning in neural networks: an overview. Neural Netw. 61, 85\u2013117 (2015)","journal-title":"Neural Netw."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Yu, Q., Yang, Y., Song, Y., Xiang, T., Hospedales, T.M.: Sketch-a-net that beats humans. In: British Machine Vision Conference (BMVC), pp. 7.1\u20137.12 (2015)","DOI":"10.5244\/C.29.7"},{"key":"19_CR3","series-title":"Lecture Notes in Mobility","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-319-19078-5_14","volume-title":"Road Vehicle Automation 2","author":"M Wagner","year":"2015","unstructured":"Wagner, M., Koopman, P.: A philosophy for developing trust in self-driving cars. In: Meyer, G., Beiker, S. (eds.) Road Vehicle Automation 2. LNMOB, pp. 163\u2013171. Springer, Cham (2015). doi: 10.1007\/978-3-319-19078-5_14"},{"key":"19_CR4","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). doi: 10.1007\/978-3-642-14295-6_24"},{"key":"19_CR5","unstructured":"Scheibler, K., Winterer, L., Wimmer, R., Becker, B.: Towards verification of artificial neural networks. In: 2015 MBMV Workshop, Chemnitz, Germany, pp. 30\u201340 (2015)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Scheibler, K., Neubauer, F., Mahdi, A., Fr\u00e4nzle, M., Teige, T., Bienm\u00fcller, T., Fehrer, D., Becker, B.: Accurate ICP-based floating-point reasoning. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 177\u2013184 (2016)","DOI":"10.1109\/FMCAD.2016.7886677"},{"key":"19_CR7","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.W., 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). doi: 10.1007\/978-3-319-63387-9_5"},{"issue":"2","key":"19_CR8","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":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). doi: 10.1007\/978-3-319-63387-9_1"},{"key":"19_CR10","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A.V., Criminisi, A.: Measuring neural net robustness with constraints. In: Annual Conference on Neural Information Processing Systems (NIPS), pp. 2613\u20132621 (2016)"},{"issue":"2","key":"19_CR11","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"JW Chinneck","year":"1991","unstructured":"Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. INFORMS J. Comput. 3(2), 157\u2013168 (1991)","journal-title":"INFORMS J. Comput."},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Jia, Y., Shelhamer, E., Donahue, J., Karayev, S., Long, J., Girshick, R., Guadarrama, S., Darrell, T.: Caffe: convolutional architecture for fast feature embedding. arXiv\/CoRR 1408.5093 arXiv:1408.5093 (2014)","DOI":"10.1145\/2647868.2654889"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Franco, J., Martin, J.: A history of satisfiability. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 3\u201374. IOS Press, February 2009","DOI":"10.3233\/978-1-58603-929-5-3"},{"key":"19_CR14","volume-title":"Decision Procedures - An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Springer, Heidelberg (2008)"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). doi: 10.1007\/11817963_11"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24605-3_37"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_49"},{"key":"19_CR18","unstructured":"Lecun, Y., Cortes, C.: The MNIST database of handwritten digits (2009)"},{"issue":"11","key":"19_CR19","doi-asserted-by":"crossref","first-page":"2278","DOI":"10.1109\/5.726791","volume":"86","author":"Y Lecun","year":"1998","unstructured":"Lecun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proc. IEEE 86(11), 2278\u20132324 (1998)","journal-title":"Proc. IEEE"},{"key":"19_CR20","unstructured":"Clevert, D., Unterthiner, T., Hochreiter, S.: Fast and accurate deep network learning by exponential linear units (ELUs). arXiv\/CoRR 1511.07289 arXiv:1511.07289 (2015)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T18:06:40Z","timestamp":1750874800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}