{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:07Z","timestamp":1779087547329,"version":"3.51.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633862","type":"print"},{"value":"9783319633879","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63387-9_5","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"97-117","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":904,"title":["Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks"],"prefix":"10.1007","author":[{"given":"Guy","family":"Katz","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[]},{"given":"Kyle","family":"Julian","sequence":"additional","affiliation":[]},{"given":"Mykel J.","family":"Kochenderfer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512\u2013526. Springer, Heidelberg (2006). doi:10.1007\/11916277_35"},{"key":"5_CR2","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"825","volume-title":"Handbook of Satisfiability","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories (Chap. 26). In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"5_CR3","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., Criminisi, A.: Measuring neural net robustness with constraints. In: Proceedings of the 30th Conference on Neural Information Processing Systems (NIPS) (2016)"},{"key":"5_CR4","unstructured":"Bojarski, M., Del Testa, D., Dworakowski, D., Firner, B., Flepp, B., Goyal, P., Jackel, L., Monfort, M., Muller, U., Zhang, J., Zhang, X., Zhao, J., Zieba, K.: End to end learning for self-driving cars, Technical report (2016). http:\/\/arxiv.org\/abs\/1604.07316"},{"key":"5_CR5","doi-asserted-by":"publisher","DOI":"10.1515\/9781400884179","volume-title":"Linear Programming and Extensions","author":"G Dantzig","year":"1963","unstructured":"Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)"},{"key":"5_CR6","unstructured":"Glorot, X., Bordes, A., Bengio, Y.: Deep sparse rectifier neural networks. In: Proceedings of the 14th International Conference on Artificial Intelligence and Statistics (AISTATS), pp. 315\u2013323 (2011)"},{"key":"5_CR7","volume-title":"Deep Learning","author":"I Goodfellow","year":"2016","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge (2016)"},{"key":"5_CR8","unstructured":"Goodfellow, I., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples, Technical report (2014). http:\/\/arxiv.org\/abs\/1412.6572"},{"issue":"6","key":"5_CR9","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.: Deep neural networks for acoustic modeling in speech recognition: the shared views of four research groups. IEEE Sig. Process. Mag. 29(6), 82\u201397 (2012)","journal-title":"IEEE Sig. Process. Mag."},{"key":"5_CR10","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks, Technical report (2016). http:\/\/arxiv.org\/abs\/1610.06940"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Jarrett, K., Kavukcuoglu, K., LeCun, Y.: What is the best multi-stage architecture for object recognition? In: Proceedings of the 12th IEEE International Conferernce on Computer Vision (ICCV), pp. 2146\u20132153 (2009)","DOI":"10.1109\/ICCV.2009.5459469"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-662-46681-0_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-B Jeannin","year":"2015","unstructured":"Jeannin, J.-B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21\u201336. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_2"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Julian, K., Lopez, J., Brush, J., Owen, M., Kochenderfer, M.: Policy compression for aircraft collision avoidance systems. In: Proceedings of the 35th Digital Avionics Systems Conference (DASC), pp. 1\u201310 (2016)","DOI":"10.1109\/DASC.2016.7778091"},{"key":"5_CR14","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex (2017). https:\/\/github.com\/guykatzz\/ReluplexCav2017"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: an efficient smt solver for verifying deep neural networks. Supplementary Material (2017). https:\/\/arxiv.org\/abs\/1702.01135","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 93\u2013100 (2016)","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"5_CR17","unstructured":"King, T.: Effective algorithms for the satisfiability of quantifier-free formulas over linear real and integer arithmetic. Ph.D. thesis, New York University (2014)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"King, T., Barret, C., Tinelli, C.: Leveraging linear and mixed integer programming for SMT. In: Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 139\u2013146 (2014)","DOI":"10.1109\/FMCAD.2014.6987606"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Kochenderfer, M.: Optimized airborne collision avoidance. In: Decision Making Under Uncertainty: Theory and Application. MIT Press, Cambridge (2015)","DOI":"10.7551\/mitpress\/10187.001.0001"},{"key":"5_CR20","unstructured":"Kochenderfer, M., Chryssanthacopoulos, J.: Robust airborne collision avoidance through dynamic programming. Project report ATC-371, Massachusetts Institute of Technology, Lincoln Laboratory (2011)"},{"issue":"2","key":"5_CR21","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.: Airspace encounter models for estimating collision risk. AIAA J. Guidance Control Dyn. 33(2), 487\u2013499 (2010)","journal-title":"AIAA J. Guidance Control Dyn."},{"issue":"1","key":"5_CR22","first-page":"17","volume":"19","author":"M Kochenderfer","year":"2012","unstructured":"Kochenderfer, M., Holland, J., Chryssanthacopoulos, J.: Next generation airborne collision avoidance system. Linc. Lab. J. 19(1), 17\u201333 (2012)","journal-title":"Linc. Lab. J."},{"key":"5_CR23","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.: Imagenet classification with deep convolutional neural networks. In: Advances in Neural Information Processing Systems, pp. 1097\u20131105 (2012)"},{"issue":"2","key":"5_CR24","first-page":"277","volume":"16","author":"J Kuchar","year":"2007","unstructured":"Kuchar, J., Drumm, A.: The traffic alert and collision avoidance system. Linc. Lab. J. 16(2), 277\u2013296 (2007)","journal-title":"Linc. Lab. J."},{"key":"5_CR25","unstructured":"Maas, A., Hannun, A., Ng, A.: Rectifier nonlinearities improve neural network acoustic models. In: Proceedings of the 30th International Conference on Machine Learning (ICML) (2013)"},{"issue":"5","key":"5_CR26","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.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"5_CR27","unstructured":"Nair, V., Hinton, G.: Rectified linear units improve restricted Boltzmann machines. In: Proceedings of the 27th International Conference on Machine Learning (ICML), pp. 807\u2013814 (2010)"},{"issue":"6","key":"5_CR28","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.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM (JACM) 53(6), 937\u2013977 (2006)","journal-title":"J. ACM (JACM)"},{"issue":"1","key":"5_CR29","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1137\/1033004","volume":"33","author":"M Padberg","year":"1991","unstructured":"Padberg, M., Rinaldi, G.: A branch-and-cut algorithm for the resolution of large-scale symmetric traveling salesman problems. SIAM Rev. 33(1), 60\u2013100 (1991)","journal-title":"SIAM Rev."},{"key":"5_CR30","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"},{"issue":"2","key":"5_CR31","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."},{"issue":"11","key":"5_CR32","doi-asserted-by":"publisher","first-page":"1019","DOI":"10.1038\/14819","volume":"2","author":"M Riesenhuber","year":"1999","unstructured":"Riesenhuber, M., Tomaso, P.: Hierarchical models of object recognition in cortex. Nat. Neurosci. 2(11), 1019\u20131025 (1999). doi:10.1038\/14819","journal-title":"Nat. Neurosci."},{"issue":"7587","key":"5_CR33","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.: Mastering the game of Go with deep neural networks and tree search. Nature 529(7587), 484\u2013489 (2016)","journal-title":"Nature"},{"key":"5_CR34","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks, Technical report (2013). http:\/\/arxiv.org\/abs\/1312.6199"},{"key":"5_CR35","volume-title":"Linear Programming: Foundations and Extensions","author":"R Vanderbei","year":"1996","unstructured":"Vanderbei, R.: Linear Programming: Foundations and Extensions. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:14:58Z","timestamp":1626135298000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}