{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:15:51Z","timestamp":1784837751652,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642239533","type":"print"},{"value":"9783642239540","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23954-0_14","type":"book-chapter","created":{"date-parts":[[2011,9,11]],"date-time":"2011-09-11T00:30:34Z","timestamp":1315701034000},"page":"127-138","source":"Crossref","is-referenced-by-count":3,"title":["Checking Safety of Neural Networks with SMT Solvers: A Comparative Evaluation"],"prefix":"10.1007","author":[{"given":"Luca","family":"Pulina","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","first-page":"825","volume-title":"Handbook of Satisfiability","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.Y., Merz, S., Nieto, L., Tiu, A.: Expressiveness+ automation+ soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"14_CR3","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs (2005)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Ray, S.: Connecting External Deduction Tools with ACL2. In: Scalable Techniques for Formal Verification, pp. 195\u2013216 (2010)","DOI":"10.1007\/978-1-4419-5998-0_14"},{"issue":"1","key":"14_CR5","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A. Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. International Journal on Software Tools for Technology Transfer (STTT)\u00a011(1), 69\u201383 (2009)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"14_CR6","first-page":"183","volume-title":"2010 Second International Conference on Knowledge and Systems Engineering (KSE)","author":"T.A. Hoang","year":"2010","unstructured":"Hoang, T.A., Binh, N.N.: Extending CREST with Multiple SMT Solvers and Real Arithmetic. In: 2010 Second International Conference on Knowledge and Systems Engineering (KSE), pp. 183\u2013187. IEEE, Los Alamitos (2010)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability Modulo Theories Competition. In: Etessami, K., Rajamani, S. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 20\u201323. Springer, Heidelberg (2005)"},{"issue":"6","key":"14_CR8","doi-asserted-by":"publisher","first-page":"1803","DOI":"10.1063\/1.1144830","volume":"65","author":"C.M. Bishop","year":"2009","unstructured":"Bishop, C.M.: Neural networks and their applications. Review of Scientific Instruments\u00a065(6), 1803\u20131832 (2009)","journal-title":"Review of Scientific Instruments"},{"key":"14_CR9","series-title":"SCI","volume-title":"Applications of Neural Networks in High Assurance Systems","year":"2010","unstructured":"Schumann, J., Liu, Y. (eds.): Applications of Neural Networks in High Assurance Systems. SCI, vol.\u00a0268. Springer, Heidelberg (2010)"},{"key":"14_CR10","volume-title":"Neural networks: a comprehensive foundation","author":"S. Haykin","year":"2008","unstructured":"Haykin, S.: Neural networks: a comprehensive foundation. Prentice Hall, Englewood Cliffs (2008)"},{"issue":"5","key":"14_CR11","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/0893-6080(89)90020-8","volume":"2","author":"K. Hornik","year":"1989","unstructured":"Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Networks\u00a02(5), 359\u2013366 (1989)","journal-title":"Neural Networks"},{"key":"14_CR12","unstructured":"Cok, D.R.: The SMT-LIBv2 Language and Tools: A Tutorial (2011), http:\/\/www.grammatech.com\/resources\/smt\/"},{"key":"14_CR13","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190012","volume":"1","author":"M. Franzle","year":"2007","unstructured":"Franzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation\u00a01, 209\u2013236 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"14_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.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"14_CR16","series-title":"SCI","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-05181-4_7","volume-title":"From Motor Learning to Interaction Learning in Robots","author":"M. Fumagalli","year":"2010","unstructured":"Fumagalli, M., Gijsberts, A., Ivaldi, S., Jamone, L., Metta, G., Natale, L., Nori, F., Sandini, G.: Learning to Exploit Proximal Force Sensing: a Comparison Approach. In: Sigaud, O., Peters, J. (eds.) From Motor Learning to Interaction Learning in Robots. SCI, vol.\u00a0264, pp. 149\u2013167. Springer, Heidelberg (2010)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","AI*IA 2011: Artificial Intelligence Around Man and Beyond"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23954-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,23]],"date-time":"2020-06-23T15:45:28Z","timestamp":1592927128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23954-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642239533","9783642239540"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23954-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}