{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T14:08:56Z","timestamp":1773842936722,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031249495","type":"print"},{"value":"9783031249501","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-24950-1_2","type":"book-chapter","created":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T14:03:19Z","timestamp":1673877799000},"page":"25-43","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["SMT-Based Modeling and\u00a0Verification of\u00a0Spiking Neural Networks: A Case Study"],"prefix":"10.1007","author":[{"given":"Soham","family":"Banerjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sumana","family":"Ghosh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ansuman","family":"Banerjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Swarup K.","family":"Mohalik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,17]]},"reference":[{"key":"2_CR1","unstructured":"Code and Benchmarks. https:\/\/github.com\/Soham-Banerjee\/SMT-Encoding-for-Spiking-Neural-Network"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R Alur","year":"1999","unstructured":"Alur, R.: Timed automata. In: Peled, D. (ed.) CAV 1999. LNCS, vol. 1633, pp. 8\u201322. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_3"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.tcs.2015.11.005","volume":"623","author":"B Aman","year":"2016","unstructured":"Aman, B., Ciobanu, G.: Modelling and verification of weighted spiking neural systems. Theoret. Comput. Sci. 623, 92\u2013102 (2016)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"De Maria, E., Di Giusto, C., Laversa, L.: Spiking neural networks modelled as timed automata with parameter learning (2018)","DOI":"10.5220\/0006530300170028"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-47151-8_7","volume-title":"Hybrid Systems Biology","author":"E De Maria","year":"2016","unstructured":"De Maria, E., Muzy, A., Gaff\u00e9, D., Ressouche, A., Grammont, F.: Verification of temporal properties of neuronal archetypes modeled as synchronous reactive systems. In: Cinquemani, E., Donz\u00e9, A. (eds.) HSB 2016. LNCS, vol. 9957, pp. 97\u2013112. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47151-8_7"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"79","DOI":"10.3389\/fninf.2018.00079","volume":"12","author":"V Demin","year":"2018","unstructured":"Demin, V., Nekhaev, D.: Recurrent spiking neural network learning based on a competitive maximization of neuronal activity. Front. Neuroinf. 12, 79 (2018)","journal-title":"Front. Neuroinf."},{"issue":"6","key":"2_CR7","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/MSP.2012.2211477","volume":"29","author":"L Deng","year":"2012","unstructured":"Deng, L.: The MNIST database of handwritten digit images for machine learning research. IEEE Signal Process. Mag. 29(6), 141\u2013142 (2012)","journal-title":"IEEE Signal Process. Mag."},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"99","DOI":"10.3389\/fncom.2015.00099","volume":"9","author":"PU Diehl","year":"2015","unstructured":"Diehl, P.U., Cook, M.: Unsupervised learning of digit recognition using spike-timing-dependent plasticity. Front. Comput. Neurosci. 9, 99 (2015)","journal-title":"Front. Comput. Neurosci."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Ding, J., Yu, Z., Tian, Y., Huang, T.: Optimal ANN-SNN conversion for fast and accurate inference in deep spiking neural networks (2021)","DOI":"10.24963\/ijcai.2021\/321"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-030-53288-8_3","volume-title":"Computer Aided Verification","author":"YY Elboher","year":"2020","unstructured":"Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 43\u201365. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_3"},{"key":"2_CR11","unstructured":"Eshraghian, J.K., et al.: Training spiking neural networks using lessons from deep learning (2021)"},{"key":"2_CR12","unstructured":"Fisher, R.: Iris. UCI Machine Learning Repository (1988). https:\/\/archive.ics.uci.edu\/ml\/datasets\/Iris"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-030-55754-6_5","volume-title":"NASA Formal Methods","author":"S Gokulanathan","year":"2020","unstructured":"Gokulanathan, S., Feldsher, A., Malca, A., Barrett, C., Katz, G.: Simplifying neural networks using formal verification. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 85\u201393. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_5"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Goldberger, B., Katz, G., Adi, Y., Keshet, J.: Minimal modifications of deep neural networks using verification. In: LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol. 73, pp. 260\u2013278 (2020)","DOI":"10.29007\/699q"},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"638474","DOI":"10.3389\/fnins.2021.638474","volume":"15","author":"W Guo","year":"2021","unstructured":"Guo, W., Fouda, M.E., Eltawil, A.M., Salama, K.N.: Neural coding in spiking neural networks: a comparative study for robust neuromorphic systems. Front. Neurosci. 15, 638474 (2021)","journal-title":"Front. Neurosci."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Design 1\u201330 (2021)","DOI":"10.1007\/s10703-021-00363-7"},{"key":"2_CR17","doi-asserted-by":"publisher","DOI":"10.3389\/fncom.2021.646125","volume":"15","author":"T Kim","year":"2021","unstructured":"Kim, T., et al.: Spiking neural network (SNN) with memristor synapses having non-linear weight update. Front. Comput. Neurosci. 15, 646125 (2021)","journal-title":"Front. Comput. Neurosci."},{"key":"2_CR18","unstructured":"Kuper, L., Katz, G., Gottschlich, J., Julian, K., Barrett, C., Kochenderfer, M.: Toward scalable verification for safety-critical deep networks (2018)"},{"key":"2_CR19","unstructured":"Lahav, O., Katz, G.: Pruning and slicing neural networks using formal verification (2021)"},{"issue":"4","key":"2_CR20","doi-asserted-by":"publisher","first-page":"1543","DOI":"10.1109\/TCSI.2021.3052885","volume":"68","author":"S Li","year":"2021","unstructured":"Li, S., Zhang, Z., Mao, R., Xiao, J., Chang, L., Zhou, J.: A fast and energy-efficient SNN processor with adaptive clock\/event-driven computation scheme and online learning. IEEE Trans. Circuits Syst. I Regul. Pap. 68(4), 1543\u20131552 (2021)","journal-title":"IEEE Trans. Circuits Syst. I Regul. Pap."},{"issue":"4","key":"2_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1371\/journal.pone.0264364","volume":"17","author":"TY Liu","year":"2022","unstructured":"Liu, T.Y., Mahjoubfar, A., Prusinski, D., Stevens, L.: Neuromorphic computing for content-based image retrieval. PLOS One 17(4), 1\u201313 (2022). https:\/\/doi.org\/10.1371\/journal.pone.0264364","journal-title":"PLOS One"},{"key":"2_CR22","unstructured":"Malik, N.: Artificial neural networks and their applications (2005)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"de Maria, E., Gaff\u00e9, D., Ressouche, A., Girard Riboulleau, C.: A model-checking approach to reduce spiking neural networks. In: BIOINFORMATICS 2018 - 9th International Conference on Bioinformatics Models, Methods and Algorithms, pp. 1\u20138 (2018)","DOI":"10.5220\/0006572000890096"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Stimberg, M., Brette, R., Goodman, D.F.: Brian 2, an intuitive and efficient neural simulator. eLife 8, e47314 (2019)","DOI":"10.7554\/eLife.47314"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Tavanaei, A., Ghodrati, M., Kheradpisheh, S.R., Masquelier, T., Maida, A.S.: Deep learning in spiking neural networks (2018)","DOI":"10.1016\/j.neunet.2018.12.002"},{"key":"2_CR27","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming (2017)"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"67085","DOI":"10.1109\/ACCESS.2020.2985839","volume":"8","author":"Z Yu","year":"2020","unstructured":"Yu, Z., Abdulghani, A.M., Zahid, A., Heidari, H., Imran, M.A., Abbasi, Q.H.: An overview of neuromorphic computing for artificial intelligence enabled hardware-based hopfield neural network. IEEE Access 8, 67085\u201367099 (2020). https:\/\/doi.org\/10.1109\/ACCESS.2020.2985839","journal-title":"IEEE Access"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-24950-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T09:08:19Z","timestamp":1728724099000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-24950-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031249495","9783031249501"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-24950-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 January 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Boston, MA","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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/vmcai-2023.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}