{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:13:46Z","timestamp":1768342426468,"version":"3.49.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030888053","type":"print"},{"value":"9783030888060","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-3-030-88806-0_8","type":"book-chapter","created":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:25:06Z","timestamp":1634145906000},"page":"166-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Static Analysis of ReLU Neural Networks with Tropical Polyhedra"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3198-1863","authenticated-orcid":false,"given":"Eric","family":"Goubault","sequence":"first","affiliation":[]},{"given":"S\u00e9bastien","family":"Palumby","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5624-3755","authenticated-orcid":false,"given":"Sylvie","family":"Putot","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1599-2431","authenticated-orcid":false,"given":"Louis","family":"Rustenholz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7315-4340","authenticated-orcid":false,"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,13]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Alemdar, H., Caldwell, N., Leroy, V., Prost-Boucle, A., P\u00e9trot, F.: Ternary neural networks for resource-efficient AI applications. CoRR abs\/1609.00222 (2016)","DOI":"10.1109\/IJCNN.2017.7966166"},{"key":"8_CR2","unstructured":"Allamigeon, X., Gaubert, S., Goubault, E.: The tropical double description method. In: 27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010 (2010)"},{"key":"8_CR3","unstructured":"Allamigeon, X.: Static analysis of memory manipulations by abstract interpretation\u00a0- Algorithmics of tropical polyhedra, and application to abstract interpretation. Ph.D. thesis, \u00c9cole Polytechnique, Palaiseau, France (2009). https:\/\/tel.archives-ouvertes.fr\/pastel-00005850"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-69166-2_13","volume-title":"Static Analysis","author":"X Allamigeon","year":"2008","unstructured":"Allamigeon, X., Gaubert, S., Goubault, \u00c9.: Inferring min and max invariants using max-plus polyhedra. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 189\u2013204. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69166-2_13"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-030-53288-8_4","volume-title":"Computer Aided Verification","author":"S Bak","year":"2020","unstructured":"Bak, S., Tran, H.-D., Hobbs, K., Johnson, T.T.: Improved geometric path enumeration for verifying ReLU neural networks. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 66\u201396. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_4"},{"key":"8_CR6","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., Criminisi, A.: Measuring neural net robustness with constraints. In: Advances in Neural Information Processing Systems (NIPS) (2016)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: PLDI, pp. 196\u2013207. ACM Press, June 2003","DOI":"10.1145\/780822.781153"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient verification of relu-based neural networks via dependency analysis. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, no. 04, pp. 3291\u20133299 (2020). https:\/\/vas.doc.ic.ac.uk\/software\/neural\/","DOI":"10.1609\/aaai.v34i04.5729"},{"issue":"4","key":"8_CR9","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1017\/S0956796800000496","volume":"2","author":"F Bourdoncle","year":"1992","unstructured":"Bourdoncle, F.: Abstract interpretation by dynamic partitioning. J. Func. Program. 2(4), 407\u2013435 (1992)","journal-title":"J. Func. Program."},{"key":"8_CR10","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: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, pp. 238\u2013252, January 1977","DOI":"10.1145\/512950.512973"},{"key":"8_CR11","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: POPL. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 84\u201396. POPL 1978, Association for Computing Machinery, New York, NY, USA (1978). https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: HSCC (2019)","DOI":"10.1145\/3302504.3311807"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Jha, S., Sankaranarayanan, S., Tiwari, A.: Sherlock - A tool for verification of neural network feedback systems: demo abstract. In: HSCC (2019)","DOI":"10.1145\/3302504.3313351"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: ATVA (2017)","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"8_CR16","unstructured":"Evtimov, I., et al..: Robust physical-world attacks on machine learning models. CoRR abs\/1707.08945 (2017). http:\/\/arxiv.org\/abs\/1707.08945"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1016\/j.laa.2006.09.019","volume":"421","author":"S Gaubert","year":"2006","unstructured":"Gaubert, S., Katz, R.: The Minkowski theorem for max-plus convex sets. Linear Algebra Appl. 421, 356\u2013369 (2006)","journal-title":"Linear Algebra Appl."},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Gawrilow, E., Joswig, M.: polymake: a Framework for Analyzing Convex Polytopes, pp. 43\u201373. Birkh\u00e4user Basel (2000)","DOI":"10.1007\/978-3-0348-8438-9_2"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: Conf\u00e9rence IEEE S&P 2018 (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"8_CR20","unstructured":"Gowal, S., et al.: On the effectiveness of interval bound propagation for training verifiably robust models. CoRR abs\/1810.12715 (2018). http:\/\/arxiv.org\/abs\/1810.12715"},{"key":"8_CR21","unstructured":"Henriksen, P., Lomuscio, A.R.: Efficient neural network verification via adaptive refinement and adversarial search. In: ECAI. Frontiers in Artificial Intelligence and Applications, vol. 325 (2020)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"8_CR23","unstructured":"Julian, K., Kochenderfer, M.J., Owen, M.P.: Deep neural network compression for aircraft collision avoidance systems. AIAA J. Guidance Control Dyn. (2018). https:\/\/arxiv.org\/pdf\/1810.04240.pdf"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: CAV 2017 (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The Marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"8_CR26","unstructured":"Khedr, H., Ferlez, J., Shoukry, Y.: Effective formal verification of neural networks using the geometry of linear regions (2020)"},{"key":"8_CR27","unstructured":"Li, F., Liu, B.: Ternary weight networks. CoRR abs\/1605.04711 (2016)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Programming Languages and Systems (2005)","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155\u2013172. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44978-7_10"},{"issue":"1","key":"8_CR30","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symb. Comput."},{"key":"8_CR31","unstructured":"M\u00fcller, M.N., Makarchuk, G., Singh, G., P\u00fcschel, M., Vechev, M.: Precise multi-neuron abstractions for neural network certification (2021)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. In: IJCAI (2018)","DOI":"10.24963\/ijcai.2018\/368"},{"key":"8_CR33","unstructured":"Shiqi, W., Pei, K., Justin, W., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: NIPS (2018)"},{"key":"8_CR34","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification"},{"key":"8_CR35","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. In: Advances in Neural Information Processing Systems (NeurIPS) (2019)"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. In: Proceedings ACM Programming Language 3(POPL), January 2019","DOI":"10.1145\/3290354"},{"key":"8_CR37","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: Boosting robustness certification of neural networks. In: ICLR (2019)"},{"key":"8_CR38","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks (2013). https:\/\/arxiv.org\/abs\/1312.6199"},{"key":"8_CR39","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. https:\/\/arxiv.org\/abs\/1711.07356"},{"key":"8_CR40","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. USENIX Security (2018)"},{"key":"8_CR41","unstructured":"Zhang, H., et al.: Towards stable and efficient training of verifiably robust neural networks. In: ICLR (2020)"},{"key":"8_CR42","unstructured":"Zhang, L., G.Naitzat, Lim, L.H.: Tropical geometry of deep neural networks. In: Proceedings of the 35th International Conference on Machine Learning, vol. 80, pp. 5824\u20135832. PMLR (2018)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88806-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:27:56Z","timestamp":1634146076000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88806-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030888053","9783030888060"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88806-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"13 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chicago, IL","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/staticanalysis.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"40","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":"18","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":"4","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":"45% - 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":"6","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)"}}]}}