{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T15:17:40Z","timestamp":1772896660140,"version":"3.50.1"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030010898","type":"print"},{"value":"9783030010904","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","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-030-01090-4_2","type":"book-chapter","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T11:23:23Z","timestamp":1538220203000},"page":"20-34","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":68,"title":["Formal Specification for Deep Neural Networks"],"prefix":"10.1007","author":[{"given":"Sanjit A.","family":"Seshia","sequence":"first","affiliation":[]},{"given":"Ankush","family":"Desai","sequence":"additional","affiliation":[]},{"given":"Tommaso","family":"Dreossi","sequence":"additional","affiliation":[]},{"given":"Daniel J.","family":"Fremont","sequence":"additional","affiliation":[]},{"given":"Shromona","family":"Ghosh","sequence":"additional","affiliation":[]},{"given":"Edward","family":"Kim","sequence":"additional","affiliation":[]},{"given":"Sumukh","family":"Shivakumar","sequence":"additional","affiliation":[]},{"given":"Marcell","family":"Vazquez-Chanlatte","sequence":"additional","affiliation":[]},{"given":"Xiangyu","family":"Yue","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,9,30]]},"reference":[{"key":"2_CR1","unstructured":"Albarghouthi, A., D\u2019Antoni, L., Drews, S., Nori, A.: Fairness as a program property (2016), arXiv:1610.06067"},{"issue":"OOPSLA","key":"2_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3133904","volume":"1","author":"Aws Albarghouthi","year":"2017","unstructured":"Albarghouthi, A., D\u2019Antoni, L., Drews, S., Nori, A.V.: Fairsquare: probabilistic verification of program fairness. In: Proceedings of the ACM on Programming Languages (2017)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1038\/nbt.3300","volume":"33","author":"B Alipanahi","year":"2015","unstructured":"Alipanahi, B., Delong, A., Weirauch, M.T., Frey, B.J.: Predicting the sequence specificities of DNA-and RNA-binding proteins by deep learning. Nat. Biotechnol. 33, 831\u2013838 (2015)","journal-title":"Nat. Biotechnol."},{"key":"2_CR4","unstructured":"Amodei, D., Olah, C., Steinhardt, J., Christiano, P.F., Schulman, J., Man\u00e9, D.: Concrete problems in AI safety. ArXiV e-prints abs\/1606.06565 (2016)"},{"key":"2_CR5","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., Criminisi, A.: Measuring neural net robustness with constraints. In: Lee, D.D., Sugiyama, M., Luxburg, U.V., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems (NIPS), vol. 29, pp. 2613\u20132621. MIT Press, Cambridge (2016)"},{"key":"2_CR6","unstructured":"Binns, R.: Fairness in machine learning: lessons from political philosophy (2017), arXiv:1712.03586"},{"key":"2_CR7","unstructured":"Bojarski, M., et al.: End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016)"},{"key":"2_CR8","unstructured":"Cai, J., Shin, R., Song, D.: Making neural programming architectures generalize via recursion. arXiv preprint arXiv:1704.06611 (2017)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Carlini, N., Wagner, D.: Towards evaluating the robustness of neural networks. In: IEEE Symposium on Security and Privacy (SP) (2017)","DOI":"10.1109\/SP.2017.49"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.18637\/jss.v076.i01","volume":"76","author":"B Carpenter","year":"2017","unstructured":"Carpenter, B., et al.: Stan: a probabilistic programming language. J. Stat. Softw. 76(1), 1\u201332 (2017)","journal-title":"J. Stat. Softw."},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-68167-2_18","volume-title":"Automated Technology for Verification and Analysis","author":"C-H Cheng","year":"2017","unstructured":"Cheng, C.-H., N\u00fchrenberg, G., Ruess, H.: Maximum resilience of artificial neural networks. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 251\u2013268. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_18"},{"issue":"6","key":"2_CR12","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Dahl, G.E., Stokes, J.W., Deng, L., Yu, D.: Large-scale malware classification using random projections and neural networks. In: Proceedings of the IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). pp. 3422\u20133426. IEEE (2013)","DOI":"10.1109\/ICASSP.2013.6638293"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Dai, J., et al.: Deformable convolutional networks. In: IEEE International Conference on Computer Vision (2017)","DOI":"10.1109\/ICCV.2017.89"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Dreossi, T., Donz\u00e9, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: NASA Formal Methods Symposium (2017)","DOI":"10.1007\/978-3-319-57288-8_26"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-57288-8_26","volume-title":"NASA Formal Methods","author":"T Dreossi","year":"2017","unstructured":"Dreossi, T., Donz\u00e9, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 357\u2013372. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_26"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Dreossi, T., Ghosh, S., Yue, X., Keutzer, K., Sangiovanni-Vincentelli, A., Seshia, S.A.: Counterexample-guided data augmentation. In: 27th International Joint Conference on Artificial Intelligence (IJCAI) (2018)","DOI":"10.24963\/ijcai.2018\/286"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-96145-3_1","volume-title":"Computer Aided Verification","author":"Tommaso Dreossi","year":"2018","unstructured":"Dreossi, T., Jha, S., Seshia, S.A.: Semantic adversarial deep learning. In: 30th International Conference on Computer Aided Verification (CAV) (2018)"},{"key":"2_CR19","unstructured":"Dutta, S., Jha, S., Sanakaranarayanan, S., Tiwari, A.: Output range analysis for deep neural networks (2017), arXiv:1709.09130"},{"key":"2_CR20","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T., Kohli, P.: A dual approach to scalable verification of deep networks (2018), arXiv:1803.06567"},{"key":"2_CR21","unstructured":"Fawzi, A., Frossard, P.: Manitest: Are classifiers really invariant? (2017), arXiv:1507.06535"},{"key":"2_CR22","unstructured":"Fremont, D., Yue, X., Dreossi, T., Ghosh, S., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: Language-based scene generation. Technical report UCB\/EECS-2018-8. EECS Department, University of California, Berkeley, April 2018. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2018\/EECS-2018-8.html"},{"key":"2_CR23","unstructured":"Friedler, S.A., Scheidegger, C., Venkatasubramanian, S.: On the (im) possibility of fairness (2016), arXiv:1609.07236"},{"key":"2_CR24","unstructured":"Friedler, S.A., Scheidegger, C., Venkatasubramanian, S., Choudhary, S., Hamilton, E.P., Roth, D.: A comparative study of fairness-enhancing interventions in machine learning (2018), arXiv:1802.04422"},{"key":"2_CR25","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge (2016). http:\/\/goodfeli.github.io\/dlbook\/"},{"key":"2_CR26","unstructured":"Goodfellow, I., Lee, H., Le, Q.V., Saxe, A., Ng, A.Y.: Measuring invariances in deep networks. In: Advances in Neural Information Processing Systems (2009)"},{"key":"2_CR27","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples (2014), arXiv:1412.6572"},{"key":"2_CR28","unstructured":"Goodman, N.D., Mansinghka, V.K., Roy, D., Bonawitz, K., Tenenbaum, J.B.: Church: a language for generative models. In: Proceedings of the Twenty-Fourth Conference on Uncertainty in Artificial Intelligence, pp. 220\u2013229. UAI\u201908 (2008)"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE 2014, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"2_CR30","unstructured":"Graves, A., Wayne, G., Danihelka, I.: Neural turing machines. arXiv preprint arXiv:1410.5401 (2014)"},{"key":"2_CR31","unstructured":"Hardt, M., Price, E., Srebro, N., et al.: Equality of opportunity in supervised learning. In: Advances in Neural Information Processing Systems (2016)"},{"key":"2_CR32","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). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"2_CR33","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1613\/jair.301","volume":"4","author":"LP Kaelbling","year":"1996","unstructured":"Kaelbling, L.P., Littman, M.L., Moore, A.W.: Reinforcement learning: a survey. J. Artif. Intell. Res. 4, 237\u2013285 (1996)","journal-title":"J. Artif. Intell. Res."},{"key":"2_CR34","unstructured":"Kanbak, C., Moosavi-Dezfooli, S.M., Frossard, P.: Geometric robustness of deep networks: analysis and improvement (2017), arXiv:1711.09115"},{"key":"2_CR35","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. In: Advances in Neural Information Processing Systems, pp. 1097\u20131105 (2012)"},{"key":"2_CR36","unstructured":"Kusner, M.J., Loftus, J., Russell, C., Silva, R.: Counterfactual fairness. In: Advances in Neural Information Processing Systems (2017)"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Lowe, D.G.: Object recognition from local scale-invariant features. In: IEEE International Conference on Computer Vision (1999)","DOI":"10.1109\/ICCV.1999.790410"},{"key":"2_CR38","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks (2017), arXiv:1706.06083"},{"key":"2_CR39","unstructured":"Milch, B., Marthi, B., Russell, S.: Blog: Relational modeling with unknown objects. In: ICML 2004 Workshop on Statistical Relational Learning and its Connections to Other Fields, pp. 67\u201373 (2004)"},{"issue":"7540","key":"2_CR40","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1038\/nature14236","volume":"518","author":"V Mnih","year":"2015","unstructured":"Mnih, V., et al.: Human-level control through deep reinforcement learning. Nature 518(7540), 529 (2015)","journal-title":"Nature"},{"key":"2_CR41","unstructured":"NVIDIA: Nvidia tegra drive px: Self-driving car computer (2015), http:\/\/www.nvidia.com\/object\/drive-px.html"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P., Jha, S., Fredrikson, M., Celik, Z.B., Swami, A.: The limitations of deep learning in adversarial settings. In: Proceedings of the 1st IEEE European Symposium on Security and Privacy. arXiv preprint arXiv:1511.07528 (2016)","DOI":"10.1109\/EuroSP.2016.36"},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P., Wu, X., Jha, S., Swami, A.: Distillation as a defense to adversarial perturbations against deep neural networks. arXiv preprint arXiv:1511.04508 (2015)","DOI":"10.1109\/SP.2016.41"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: automated whitebox testing of deep learning systems. In: Proceedings of the 26th Symposium on Operating Systems Principles, pp. 1\u201318. ACM (2017)","DOI":"10.1145\/3132747.3132785"},{"key":"2_CR45","unstructured":"Pfeffer, A.: Figaro: an object-oriented probabilistic programming language. Technical report, Charles River Analytics (2009)"},{"key":"2_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-45720-8_19","volume-title":"Connectionist Models of Neurons, Learning Processes, and Artificial Intelligence","author":"P Rodrigues","year":"2001","unstructured":"Rodrigues, P., Costa, J.F., Siegelmann, H.T.: Verifying properties of neural networks. In: Mira, J., Prieto, A. (eds.) IWANN 2001. LNCS, vol. 2084, pp. 158\u2013165. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45720-8_19"},{"issue":"4","key":"2_CR47","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1609\/aimag.v36i4.2621","volume":"36","author":"S Russell","year":"2015","unstructured":"Russell, S., et al.: Letter to the editor: research priorities for robust and beneficial artif icial intelligence: an open letter. AI Mag. 36(4), 3\u20134 (2015)","journal-title":"AI Mag."},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"Sadigh, D., Kim, E.S., Coogan, S., Sastry, S., Seshia, S.A.: A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In: Proceedings of the 53rd IEEE Conference on Decision and Control (CDC), pp. 1091\u20131096, December 2014","DOI":"10.1109\/CDC.2014.7039527"},{"key":"2_CR49","unstructured":"Selsam, D., Liang, P., Dill, D.L.: Developing bug-free machine learning systems with formal mathematics. In: International Conference on Machine Learning, pp. 3047\u20133056 (2017)"},{"key":"2_CR50","unstructured":"Seshia, S.A.: Compositional verification without compositional specification for learning-based systems. Technical report UCB\/EECS-2017-164. EECS Department, University of California, Berkeley, November 2017. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2017\/EECS-2017-164.html"},{"key":"2_CR51","unstructured":"Seshia, S.A., et al.: Formal specification for deep neural networks. Technical report UCB\/EECS-2018-25. EECS Department, University of California, Berkeley, May 2018. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2018\/EECS-2018-25.html"},{"key":"2_CR52","unstructured":"Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards Verified Artificial Intelligence. ArXiv e-prints, July 2016"},{"key":"2_CR53","unstructured":"Shin, E.C.R., Song, D., Moazzezi, R.: Recognizing functions in binaries with neural networks. In: 24th USENIX Security Symposium (USENIX Security 15), pp. 611\u2013626 (2015)"},{"key":"2_CR54","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks (2013), arXiv:1312.6199"},{"key":"2_CR55","doi-asserted-by":"crossref","unstructured":"Taylor, B.J., Darrah, M.A.: Rule extraction as a formal method for the verification and validation of neural networks. In: IEEE International Joint Conference on Neural Networks (IJCNN), vol. 5, pp. 2915\u20132920. IEEE (2005)","DOI":"10.1109\/IJCNN.2005.1556388"},{"key":"2_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_24"},{"key":"2_CR57","doi-asserted-by":"crossref","unstructured":"Wen, M., Ehlers, R., Topcu, U.: Correct-by-synthesis reinforcement learning with temporal logic constraints. In: 2015 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 4983\u20134990 (2015)","DOI":"10.1109\/IROS.2015.7354078"},{"key":"2_CR58","unstructured":"Weng, T.W., et al.: Evaluating the robustness of neural networks: an extreme value theory approach (2018), arXiv:1801.10578"},{"key":"2_CR59","unstructured":"You, S., Ding, D., Canini, K., Pfeifer, J., Gupta, M.: Deep lattice networks and partial monotonic functions. In: Advances in Neural Information Processing Systems (2017)"}],"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-030-01090-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,21]],"date-time":"2025-10-21T14:46:54Z","timestamp":1761058014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-01090-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030010898","9783030010904"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01090-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}