{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:59:45Z","timestamp":1764403185412,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031158384"},{"type":"electronic","value":"9783031158391"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-15839-1_14","type":"book-chapter","created":{"date-parts":[[2022,8,28]],"date-time":"2022-08-28T18:02:38Z","timestamp":1661709758000},"page":"237-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["On Neural Network Equivalence Checking Using SMT Solvers"],"prefix":"10.1007","author":[{"given":"Charis","family":"Eleftheriadis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolaos","family":"Kekatos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,29]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A.: Introduction to neural network verification. Found. Trends\u00ae Program. Lang. 7(1\u20132), 1\u2013157 (2021)","DOI":"10.1561\/2500000051"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-030-72013-1_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Amir","year":"2021","unstructured":"Amir, G., Wu, H., Barrett, C., Katz, G.: An SMT-based approach for verifying binarized neural networks. In: TACAS 2021. LNCS, vol. 12652, pp. 203\u2013222. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_11"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-030-59152-6_5","volume-title":"Automated Technology for Verification and Analysis","author":"P Ashok","year":"2020","unstructured":"Ashok, P., Hashemi, V., K\u0159et\u00ednsk\u00fd, J., Mohr, S.: DeepAbstract: neural network abstraction for accelerating verification. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 92\u2013107. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_5"},{"key":"14_CR4","unstructured":"Bak, S., Liu, C., Johnson, T.: The second international verification of neural networks competition (VNN-COMP 2021): summary and results (2021)"},{"key":"14_CR5","first-page":"825","volume-title":"Handbook of Satisfiability","author":"CW Barrett","year":"2009","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"issue":"5","key":"14_CR6","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1002\/widm.1157","volume":"5","author":"H Borchani","year":"2015","unstructured":"Borchani, H., Varando, G., Bielza, C., Larra\u00f1aga, P.: A survey on multi-output regression. Wiley Int. Rev. Data Min. Knowl. Disc. 5(5), 216\u2013233 (2015)","journal-title":"Wiley Int. Rev. Data Min. Knowl. Disc."},{"issue":"1","key":"14_CR7","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.jcss.2013.03.007","volume":"80","author":"R Cerri","year":"2014","unstructured":"Cerri, R., Barros, R.C., de Carvalho, A.C.P.L.F.: Hierarchical multi-label classification using local neural networks. J. Comput. Syst. Sci. 80(1), 39\u201356 (2014)","journal-title":"J. Comput. Syst. Sci."},{"key":"14_CR8","unstructured":"Cheng, Y., Wang, D., Zhou, P., Zhang, T.: A survey of model compression and acceleration for deep neural networks. arXiv preprint arXiv:1710.09282 (2017)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-030-81685-8_9","volume-title":"Computer Aided Verification","author":"M Christakis","year":"2021","unstructured":"Christakis, M., et al.: Automated safety verification of programs invoking neural networks. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 201\u2013224. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_9"},{"key":"14_CR10","unstructured":"Collobert, R.: Large scale machine learning. PhD thesis, Universit\u00e9 Paris VI (2004)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Deng, J., Dong, W., Socher, R., Li, L.-J., Li, K., Fei-Fei, L.: Imagenet: a large-scale hierarchical image database. In: 2009 IEEE Conference on Computer Vision and Pattern Recognition, pp. 248\u2013255 (2009)","DOI":"10.1109\/CVPR.2009.5206848"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Disch, S., Scholl, C.: Combinational equivalence checking using incremental sat solving, output ordering, and resets. In: 2007 Asia and South Pacific Design Automation Conference, pp. 938\u2013943 (2007)","DOI":"10.1109\/ASPDAC.2007.358110"},{"key":"14_CR13","unstructured":"Goldberg, E.I., Prasad, M.R., Brayton, R.K.: Using SAT for combinational equivalence checking. In: Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001, pp. 114\u2013121 (2001)"},{"key":"14_CR14","volume-title":"Advances in Neural Information Processing Systems","author":"I Goodfellow","year":"2014","unstructured":"Goodfellow, I., et al.: Generative adversarial nets. In: Ghahramani, Z., Welling, M., Cortes, C., Lawrence, N., Weinberger, K.Q. (eds.) Advances in Neural Information Processing Systems, vol. 27. Curran Associates Inc., Red Hook (2014)"},{"key":"14_CR15","unstructured":"Hinton, G., Vinyals, O., Dean, J.: Distilling the knowledge in a neural network. In: NIPS Deep Learning and Representation Learning Workshop (2015)"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"100270","DOI":"10.1016\/j.cosrev.2020.100270","volume":"37","author":"X Huang","year":"2020","unstructured":"Huang, X., et al.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020)","journal-title":"Comput. Sci. Rev."},{"key":"14_CR17","volume-title":"Advances in Neural Information Processing Systems","author":"I Hubara","year":"2016","unstructured":"Hubara, I., Courbariaux, M., Soudry, D., El-Yaniv, R., Bengio, Y.: Binarized neural networks. In: Lee, D., Sugiyama, M., Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol. 29. Curran Associates Inc., Red Hook (2016)"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"868","DOI":"10.1007\/978-3-030-58475-7_50","volume-title":"Principles and Practice of Constraint Programming","author":"M Kleine B\u00fcning","year":"2020","unstructured":"Kleine B\u00fcning, M., Kern, P., Sinz, C.: Verifying equivalence properties of neural networks with ReLU activation functions. In: Simonis, H. (ed.) CP 2020. LNCS, vol. 12333, pp. 868\u2013884. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_50"},{"key":"14_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-74105-3","edition":"1"},{"key":"14_CR21","unstructured":"Kukacka, J., Golkov, V., Cremers, D.: Regularization for deep learning: a taxonomy. arXiv, abs\/1710.10686 (2017)"},{"key":"14_CR22","unstructured":"Leofante, F., Narodytska, N., Pulina, L., Tacchella, A.: Automated verification of neural networks: advances, challenges and perspectives (2018)"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. Found. Trends\u00ae Optim. 4(3\u20134), 244\u2013404 (2021)","DOI":"10.1561\/2400000035"},{"key":"14_CR24","unstructured":"Martins, A., Astudillo, R.: From softmax to sparsemax: a sparse model of attention and multi-label classification. In: International Conference on Machine Learning, pp. 1614\u20131623. PMLR (2016)"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: Proceedings of the 2006 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 2006, pp. 836\u2013843. Association for Computing Machinery, New York (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"14_CR26","unstructured":"Mishra, R., Gupta, H.P., Dutta, T.: A survey on deep neural network compression: challenges, overview, and solutions. arXiv preprint arXiv:2010.03954 (2020)"},{"key":"14_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/b105298","volume-title":"Equivalence Checking of Digital Circuits","author":"P Molitor","year":"2004","unstructured":"Molitor, P., Mohnke, J., Becker, B., Scholl, C.: Equivalence Checking of Digital Circuits. Springer, New York (2004). https:\/\/doi.org\/10.1007\/b105298"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Kasiviswanathan, S., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence (2018)","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"14_CR29","unstructured":"Neill, J.O.: An overview of neural network compression. arXiv preprint arXiv:2006.03669 (2020)"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, C.: Reludiff: differential verification of deep neural networks. In: Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering, pp. 714\u2013726 (2020)","DOI":"10.1145\/3377811.3380337"},{"key":"14_CR31","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-0-387-73543-6_14","volume-title":"The Electronic Design Automation Handbook","author":"W R\u00fclling","year":"2003","unstructured":"R\u00fclling, W.: Formal verification. In: Jansen, D. (ed.) The Electronic Design Automation Handbook, pp. 329\u2013338. Springer, Boston (2003). https:\/\/doi.org\/10.1007\/978-0-387-73543-6_14"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL), 1\u201330 (2019)","DOI":"10.1145\/3290354"},{"key":"14_CR33","volume-title":"Electronic Design Automation For Integrated Circuits Handbook","author":"F Somenzi","year":"2016","unstructured":"Somenzi, F., Kuehlmann, A.: Equivalence checking. In: Lavagno, L., Martin, G.E., Scheffer, L.K., Markov, I.L. (eds.) Electronic Design Automation For Integrated Circuits Handbook, vol. 2. CRC Press, Boca Raton (2016)"},{"key":"14_CR34","unstructured":"Sotoudeh, M., Thakur, A.V.: A symbolic neural network representation and its application to understanding, verifying, and patching networks. CoRR, abs\/1908.06223 (2019)"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Teuber, S., B\u00fcning, M.K., Kern, P., Sinz, C.: Geometric path enumeration for equivalence verification of neural networks. In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI), pp. 200\u2013208. IEEE (2021)","DOI":"10.1109\/ICTAI52525.2021.00035"},{"key":"14_CR36","unstructured":"Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. In: Advances in Neural Information Processing Systems, vol. 34 (2021)"},{"key":"14_CR37","unstructured":"Wehrmann, J., Cerri, R., Barros, R.: Hierarchical multi-label classification networks. In: Dy, J., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 80, pp. 5075\u20135084. PMLR (2018)"},{"key":"14_CR38","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1016\/B978-0-12-374364-0.50016-3","volume-title":"Electronic Design Automation","author":"HPC Wen","year":"2009","unstructured":"Wen, H.P.C., Wang, L.C., Cheng, K.T.T.: Functional verification. In: Wang, L.-T., Chang, Y.-W., Cheng, K.-T.T. (eds.) Electronic Design Automation, pp. 513\u2013573. Morgan Kaufmann, Boston (2009)"},{"key":"14_CR39","unstructured":"Xiang, W., et al.: Verification for machine learning, autonomy, and neural networks survey. arXiv preprint arXiv:1810.01989 (2018)"},{"issue":"7","key":"14_CR40","first-page":"2409","volume":"31","author":"D Xu","year":"2019","unstructured":"Xu, D., Shi, Y., Tsang, I.W., Ong, Y.-S., Gong, C., Shen, X.: Survey on multi-output learning. IEEE Trans. Neural Netw. Learn. Syst. 31(7), 2409\u20132429 (2019)","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"key":"14_CR41","unstructured":"Xu, K., et al.: Fast and complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: International Conference on Learning Representations (2021)"},{"key":"14_CR42","unstructured":"Zhang, H., Weng, T.-W., Chen, P.-Y., Hsieh, C.-J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems, vol. 31 (2018)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15839-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,1]],"date-time":"2022-09-01T23:17:00Z","timestamp":1662074220000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15839-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031158384","9783031158391"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15839-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Warsaw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"formats2022","order":10,"name":"conference_id","label":"Conference ID","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":"30","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":"12","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":"2","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":"40% - 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":"3","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)"}}]}}