{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T14:08:49Z","timestamp":1773842929493,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,13]]},"DOI":"10.1145\/3735452.3735525","type":"proceedings-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T15:11:16Z","timestamp":1749827476000},"page":"40-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Modeling and Verification of Sigma Delta Neural Networks using Satisfiability Modulo Theory"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-2137-9010","authenticated-orcid":false,"given":"Sirshendu","family":"Das","sequence":"first","affiliation":[{"name":"Indian Statistical Institute, Kolkata, India"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0220-646X","authenticated-orcid":false,"given":"Ansuman","family":"Banerjee","sequence":"additional","affiliation":[{"name":"Indian Statistical Institute, Kolkata, India"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6167-9892","authenticated-orcid":false,"given":"Swarup Kumar","family":"Mohalik","sequence":"additional","affiliation":[{"name":"Ericsson India Pvt. Ltd., Bangalore, India"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2807385"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1561\/9781680839111"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","unstructured":"Soham Banerjee. 2023. SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study. 25\u201343. isbn:978-3-031-24949-5 https:\/\/doi.org\/10.1007\/978-3-031-24950-1_2 10.1007\/978-3-031-24950-1_2","DOI":"10.1007\/978-3-031-24950-1_2"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_3_2_2_5_1","unstructured":"Mariusz Bojarski. 2016. End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316."},{"key":"e_1_3_2_2_6_1","unstructured":"Mariusz Bojarski. 2017. Explaining how a deep neural network trained with end-to-end learning steers a car. arXiv preprint arXiv:1704.07911."},{"key":"e_1_3_2_2_7_1","first-page":"1","article-title":"Branch and bound for piecewise linear neural network verification","volume":"21","author":"Bunel Rudy","year":"2020","unstructured":"Rudy Bunel. 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21, 42 (2020), 1\u201339.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems. 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2012.2211477"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMOCODE63347.2024.00017"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0893-6080(89)90020-8"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.2514\/1.G003724"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00363-7"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2017.17"},{"key":"e_1_3_2_2_15_1","volume-title":"Sigma Delta Quantized Networks. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=HkNRsU5ge","author":"O\u2019Connor Peter","year":"2017","unstructured":"Peter O\u2019Connor and Max Welling. 2017. Sigma Delta Quantized Networks. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=HkNRsU5ge"},{"key":"e_1_3_2_2_16_1","volume-title":"Abstraction based Output Range Analysis for Neural Networks. CoRR, abs\/2007.09527","author":"Prabhakar Pavithra","year":"2020","unstructured":"Pavithra Prabhakar. 2020. Abstraction based Output Range Analysis for Neural Networks. CoRR, abs\/2007.09527 (2020), arXiv:2007.09527. arxiv:2007.09527"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2023.3251841"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-019-1677-2"},{"key":"e_1_3_2_2_19_1","unstructured":"Christian Szegedy. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199."},{"key":"e_1_3_2_2_20_1","unstructured":"Vincent Tjeng. 2017. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356."},{"key":"e_1_3_2_2_21_1","first-page":"29909","article-title":"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification","volume":"34","author":"Wang Shiqi","year":"2021","unstructured":"Shiqi Wang. 2021. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. NeurIPS, 34 (2021), 29909\u201329921.","journal-title":"NeurIPS"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Haoze Wu. 2024. Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In CAV. 249\u2013264. http:\/\/theory.stanford.edu\/~barrett\/pubs\/WIZ+24.pdf Montreal Canada","DOI":"10.1007\/978-3-031-65630-9_13"},{"key":"e_1_3_2_2_23_1","unstructured":"Kaidi Xu. 2020. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. arXiv preprint arXiv:2011.13824."},{"key":"e_1_3_2_2_24_1","volume-title":"Efficient neural network robustness certification with general activation functions. NeurIPS, 31","author":"Zhang Huan","year":"2018","unstructured":"Huan Zhang. 2018. Efficient neural network robustness certification with general activation functions. NeurIPS, 31 (2018)."}],"event":{"name":"LCTES '25: 26th ACM SIGPLAN\/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems","location":"Seoul Republic of Korea","acronym":"LCTES '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 26th ACM SIGPLAN\/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3735452.3735525","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T18:17:09Z","timestamp":1762280229000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3735452.3735525"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,13]]},"references-count":24,"alternative-id":["10.1145\/3735452.3735525","10.1145\/3735452"],"URL":"https:\/\/doi.org\/10.1145\/3735452.3735525","relation":{},"subject":[],"published":{"date-parts":[[2025,6,13]]},"assertion":[{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}