{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T22:43:36Z","timestamp":1784328216300,"version":"3.55.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2011,7]]},"DOI":"10.1007\/s10472-011-9243-0","type":"journal-article","created":{"date-parts":[[2012,1,17]],"date-time":"2012-01-17T08:16:32Z","timestamp":1326788192000},"page":"403-425","source":"Crossref","is-referenced-by-count":19,"title":["NeVer: a tool for artificial neural networks verification"],"prefix":"10.1007","volume":"62","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","published-online":{"date-parts":[[2012,1,18]]},"reference":[{"issue":"4","key":"9243_CR1","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1109\/5326.897072","volume":"30","author":"GP Zhang","year":"2000","unstructured":"Zhang, G.P.: Neural networks for classification: a survey. IEEE Trans. Syst. Man Cybern., Part C Appl. Rev. 30(4), 451\u2013462 (2000)","journal-title":"IEEE Trans. Syst. Man Cybern., Part C Appl. Rev."},{"key":"9243_CR2","unstructured":"Smith, D.J., Simpson, K.G.L.: Functional Safety \u2013 A Straightforward Guide to Applying IEC 61505 and Related Standards (2nd edn.). Elsevier (2004)"},{"key":"9243_CR3","unstructured":"Schumann, J., Gupta, P., Nelson, S.: On verification & validation of neural network based controllers. In: Proc. of International Conf. on Engineering Applications of Neural Networks (EANN\u201903) (2003)"},{"issue":"1","key":"9243_CR4","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/s00521-006-0039-9","volume":"16","author":"Z Kurd","year":"2007","unstructured":"Kurd, Z., Kelly, T., Austin, J.: Developing artificial neural networks for safety critical systems. Neural Comput. Appl. 16(1), 11\u201319 (2007)","journal-title":"Neural Comput. Appl."},{"issue":"2","key":"9243_CR5","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"9243_CR6","doi-asserted-by":"crossref","unstructured":"Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: International Symposium on Programming, pp. 337\u2013351. Springer (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"9243_CR7","doi-asserted-by":"crossref","unstructured":"Schubert, T.: High level formal verification of next-generation microprocessors. In: Proceedings of the 40th annual Design Automation Conference. ACM (2003)","DOI":"10.1145\/775832.775834"},{"key":"9243_CR8","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: Technology transfer of formal methods inside Microsoft. In: Integrated Formal Methods, pp. 1\u201320. Springer (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"9243_CR9","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L.: LTL model checking for security protocols. In: 20th IEEE Computer Security Foundations Symposium, pp. 385\u2013396 (2007)","DOI":"10.1109\/CSF.2007.24"},{"key":"9243_CR10","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Ho, P.: Automatic symbolic verification of embedded systems. In: IEEE Real-Time Systems Symposium, pp. 2\u201311 (1993)","DOI":"10.1109\/REAL.1993.393520"},{"key":"9243_CR11","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. Springer (1999)"},{"issue":"5","key":"9243_CR12","doi-asserted-by":"crossref","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 Netw 2(5), 359\u2013366 (1989)","journal-title":"Neural Netw"},{"key":"9243_CR13","doi-asserted-by":"crossref","unstructured":"Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: 22nd International Conference on Computer Aided Verification (CAV 2010). Lecture Notes in Computer Science, vol. 6174, pp. 243\u2013257. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"9243_CR14","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 136\u2013148. ACM (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"9243_CR15","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.G.: Abstraction-guided synthesis of synchronization. In: 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 327\u2013338. ACM (2010)","DOI":"10.1145\/1706299.1706338"},{"key":"9243_CR16","first-page":"993","volume":"9","author":"C Igel","year":"2008","unstructured":"Igel, C., Glasmachers, T., Heidrich-Meisner, V.: Shark. J. Mach. Learn. Res. 9, 993\u2013996 (2008)","journal-title":"J. Mach. Learn. Res."},{"key":"9243_CR17","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. JSAT, Boolean Modeling and Computation 1, 209\u2013236 (2007)","journal-title":"JSAT, Boolean Modeling and Computation"},{"issue":"12","key":"9243_CR18","doi-asserted-by":"crossref","first-page":"1797","DOI":"10.1016\/S0008-8846(98)00165-3","volume":"28","author":"IC Yeh","year":"1998","unstructured":"Yeh, I.C.: Modeling of strength of high-performance concrete using artificial neural networks. Cem. Concr. Res. 28(12), 1797\u20131808 (1998)","journal-title":"Cem. Concr. Res."},{"key":"9243_CR19","unstructured":"Haykin, S.: Neural Networks: a Comprehensive Foundation. Prentice Hall (2008)"},{"issue":"1","key":"9243_CR20","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0004-3702(77)90007-8","volume":"8","author":"AK Mackworth","year":"1977","unstructured":"Mackworth, A.K.: Consistency in networks of relations. Artif. Intell. 8(1), 99\u2013118 (1977)","journal-title":"Artif. Intell."},{"key":"9243_CR21","doi-asserted-by":"crossref","unstructured":"Van Hentenryck, P.: Numerica: a modeling language for global optimization. In: Fifteenth International Joint Conference on Artificial Intelligence (IJCAI), pp. 1642\u20131650 (1997)","DOI":"10.7551\/mitpress\/5073.001.0001"},{"key":"9243_CR22","unstructured":"Rossi, F., Van Beek, P., Walsh, T.: Handbook of Constraint Programming. Elsevier Science Ltd (2006)"},{"key":"9243_CR23","doi-asserted-by":"crossref","unstructured":"Barichard, V., Hao, J.K.: A population and interval constraint propagation algorithm. In: Evolutionary Multi-Criterion Optimization, Second International Conference (EMO 2003), pp. 88\u2013101. Springer (2003)","DOI":"10.1007\/3-540-36970-8_7"},{"key":"9243_CR24","first-page":"131","volume-title":"Conflict-driven Clause Learning SAT Solvers. Handbook of Satisfiability","author":"J Marques-Silva","year":"2009","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven Clause Learning SAT Solvers. Handbook of Satisfiability, pp. 131\u2013153. IOS Press, Amsterdam (2009)"},{"key":"9243_CR25","first-page":"825","volume-title":"Satisfiability Modulo Theories. Handbook of Satisfiability","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. Handbook of Satisfiability, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"9243_CR26","unstructured":"Jermann, C., Sam-Haroud, D., Trombettoni, G. (eds.): CP Workshop on Interval Analysis, Constraint Propagation, Applications (IntCP 2009) (2009)"},{"key":"9243_CR27","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"5","key":"9243_CR28","doi-asserted-by":"crossref","first-page":"794","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM (JACM) 50(5), 794 (2003)","journal-title":"J. ACM (JACM)"},{"key":"9243_CR29","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1145\/1150402.1150531","volume-title":"12th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD\u201906)","author":"I Mierswa","year":"2006","unstructured":"Mierswa, I., Wurst, M., Klinkenberg, R., Scholz, M., Euler, T.: Yale: rapid prototyping for complex data mining tasks. In: 12th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD\u201906), pp. 935\u2013940. ACM, New York (2006)"},{"key":"9243_CR30","unstructured":"Gordeau, R.: Roboop \u2013 a robotics object oriented package in C++. http:\/\/www.cours.polymtl.ca\/roboop (2005)"},{"key":"9243_CR31","doi-asserted-by":"crossref","unstructured":"Rabunal, J.R., Dorrado, J.: Artificial Neural Networks in Real-life Applications. Idea Group Pub (2006)","DOI":"10.4018\/978-1-59140-902-1"},{"key":"9243_CR32","unstructured":"Witten, I.H., Frank, E.: Data Mining (2nd edn.). Morgan Kaufmann (2005)"},{"issue":"1","key":"9243_CR33","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1613\/jair.720","volume":"13","author":"DF Gordon","year":"2000","unstructured":"Gordon, D.F.: Asimovian adaptive agents. J. Artif. Intell. Res. 13(1), 95\u2013153 (2000)","journal-title":"J. Artif. Intell. Res."},{"key":"9243_CR34","unstructured":"Pappas, G., Kress-Gazit, H. (eds.): ICRA Workshop on Formal Methods in Robotics and Automation (2009)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9243-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-011-9243-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9243-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,18]],"date-time":"2025-03-18T22:13:53Z","timestamp":1742336033000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-011-9243-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":34,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2011,7]]}},"alternative-id":["9243"],"URL":"https:\/\/doi.org\/10.1007\/s10472-011-9243-0","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7]]}}}