{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T01:31:12Z","timestamp":1769736672573,"version":"3.49.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2024,6,17]],"date-time":"2024-06-17T00:00:00Z","timestamp":1718582400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,6,17]],"date-time":"2024-06-17T00:00:00Z","timestamp":1718582400000},"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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1007\/s10703-024-00457-y","type":"journal-article","created":{"date-parts":[[2024,6,17]],"date-time":"2024-06-17T19:02:15Z","timestamp":1718650935000},"page":"178-199","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["The hexatope and octatope abstract domains for neural network verification"],"prefix":"10.1007","volume":"64","author":[{"given":"Stanley","family":"Bak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor","family":"Dohmen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashutosh","family":"Trivedi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alvaro","family":"Velasquez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,17]]},"reference":[{"key":"457_CR1","volume-title":"Network flows: theory, algorithms, and applications","author":"RK Ahuja","year":"1993","unstructured":"Ahuja RK, Magnanti TL, Orlin JB (1993) Network flows: theory, algorithms, and applications. Prentice Hall, Upper Saddle River"},{"key":"457_CR2","unstructured":"Akintunde M, Lomuscio A, Maganti L, Pirovano E (2018). Reachability analysis for neural agent-environment systems. In: 16th international conference on principles of knowledge representation and reasoning"},{"key":"457_CR3","doi-asserted-by":"crossref","unstructured":"Albarghouthi A (2021) Introduction to neural network verification. http:\/\/verifieddeeplearning.com","DOI":"10.1561\/9781680839111"},{"key":"457_CR4","doi-asserted-by":"crossref","unstructured":"Bak S (2021) nnenum: verification of ReLU neural networks with optimized abstraction refinement. In: NASA formal methods symposium, pp 19\u201336. Springer","DOI":"10.1007\/978-3-030-76384-8_2"},{"key":"457_CR5","doi-asserted-by":"crossref","unstructured":"Bak S, Dohmen T, Subramani K, Trivedi A, Velasquez A, Wojciechowski P (2023) The octatope abstract domain for verification of neural networks. In: Chechik M, Katoen J-P, Leucker M (eds), Formal methods\u201425th international symposium, FM 2023, L\u00fcbeck, Germany, March 6-10, 2023, Proceedings, volume 14000 of Lecture Notes in Computer Science, pp 454\u2013472. Springer","DOI":"10.1007\/978-3-031-27481-7_26"},{"key":"457_CR6","unstructured":"Bak S, Liu C, Johnson T (2021) The second international verification of neural networks competition (VNN-comp 2021): summary and results. arXiv:2109.00498"},{"key":"457_CR7","doi-asserted-by":"crossref","unstructured":"Bak S, Tran H-D, Hobbs K, Johnson TT (2020) Improved geometric path enumeration for verifying Relu neural networks. In: Proceedings of the 32nd international conference on computer aided verification. Springer","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"457_CR8","doi-asserted-by":"crossref","unstructured":"Baluta T, Shen S, Shinde S, Meel KS, Saxena P (2019) Quantitative verification of neural networks and its security applications. In: Proceedings of the 2019 ACM SIGSAC conference on computer and communications security, pp 1249\u20131264","DOI":"10.1145\/3319535.3354245"},{"key":"457_CR9","volume-title":"Linear programming and network flows","author":"MS Bazaraa","year":"2008","unstructured":"Bazaraa MS, Jarvis JJ, Sherali HD (2008) Linear programming and network flows. Wiley, New York"},{"key":"457_CR10","doi-asserted-by":"crossref","unstructured":"Behrmann G, David A, Larsen KG, H\u00e5kansson J, Pettersson P, Yi W, Hendriks M (2006) UPPAAL 4.0. In: 3rd international conference on the quantitative evaluation of systems (QEST 2006), 11-14 September 2006, Riverside, California, USA, pp 125\u2013126. IEEE Computer Society","DOI":"10.1109\/QEST.2006.59"},{"key":"457_CR11","doi-asserted-by":"crossref","unstructured":"Biswas S, Rajan H (2023) Fairify: fairness verification of neural networks. In: 2023 IEEE\/ACM 45th international conference on software engineering (ICSE), pp 1546\u20131558. IEEE","DOI":"10.1109\/ICSE48619.2023.00134"},{"key":"457_CR12","doi-asserted-by":"crossref","unstructured":"Casadio M, Komendantskaya E, Daggitt ML, Kokke W, Katz G, Amir G, Refaeli I (2022) Neural network robustness as a verification property: a principled case study. In: International conference on computer aided verification, pp 219\u2013231. Springer","DOI":"10.1007\/978-3-031-13185-1_11"},{"issue":"1","key":"457_CR13","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/3424305","volume":"68","author":"MB Cohen","year":"2021","unstructured":"Cohen MB, Lee YT, Song Z (2021) Solving linear programs in the current matrix multiplication time. J ACM 68(1):3:1-3:39","journal-title":"J ACM"},{"key":"457_CR14","volume-title":"Introduction to algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen TH, Leiserson CE, Rivest RL, Stein C (2009) Introduction to algorithms, 3rd edn. MIT Press, Cambridge","edition":"3"},{"key":"457_CR15","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages, POPL \u201977, pp 238\u2013252, New York, NY, USA. Association for Computing Machinery","DOI":"10.1145\/512950.512973"},{"key":"457_CR16","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008). Z3: an efficient SMT solver. In: International conference on tools and algorithms for the construction and analysis of systems, pp 337\u2013340. Springer","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"457_CR17","doi-asserted-by":"crossref","unstructured":"Duggirala PS, Viswanathan M (2016). Parsimonious, simulation based verification of linear systems. In: International conference on computer aided verification, pp 477\u2013494. Springer","DOI":"10.1007\/978-3-319-41528-4_26"},{"key":"457_CR18","doi-asserted-by":"crossref","unstructured":"Friedmann O, Hansen TD, Zwick U (2011) Subexponential lower bounds for randomized pivoting rules for the simplex algorithm. In: Symposium on theory of computing, STOC\u201911, pp 283\u2013292, New York, NY, USA. ACM","DOI":"10.1145\/1993636.1993675"},{"key":"457_CR19","doi-asserted-by":"crossref","unstructured":"Gehr T, Mirman M, Drachsler-Cohen D, Tsankov P, Chaudhuri S, Vechev M (2018). Ai2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE symposium on security and privacy (SP), pp 3\u201318. IEEE","DOI":"10.1109\/SP.2018.00058"},{"key":"457_CR20","doi-asserted-by":"crossref","unstructured":"Ghorbal K, Goubault E, Putot S (2009). The zonotope abstract domain Taylor1+. In: International conference on computer aided verification, pp 627\u2013633. Springer","DOI":"10.1007\/978-3-642-02658-4_47"},{"issue":"4","key":"457_CR21","doi-asserted-by":"publisher","first-page":"873","DOI":"10.1145\/76359.76368","volume":"36","author":"AV Goldberg","year":"1989","unstructured":"Goldberg AV, Tarjan RE (1989) Finding minimum-cost circulations by canceling negative cycles. J ACM 36(4):873\u2013886","journal-title":"J ACM"},{"key":"457_CR22","unstructured":"Henriksen P, Lomuscio A (2020). Efficient neural network verification via adaptive refinement and adversarial search. In: ECAI 2020, pp 2513\u20132520. IOS Press"},{"key":"457_CR23","doi-asserted-by":"crossref","unstructured":"Henriksen P, Lomuscio A (2021). Deepsplit: an efficient splitting method for neural network verification via indirect effect analysis. In: Proceedings of the 30th international joint conference on artificial intelligence (IJCAI21), To appear","DOI":"10.24963\/ijcai.2021\/351"},{"key":"457_CR24","doi-asserted-by":"publisher","first-page":"100270","DOI":"10.1016\/j.cosrev.2020.100270","volume":"37","author":"X Huang","year":"2020","unstructured":"Huang X, Kroening D, Ruan W, Sharp J, Sun Y, Thamo E, Wu M, Yi X (2020) A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput Sci Rev 37:100270","journal-title":"Comput Sci Rev"},{"key":"457_CR25","doi-asserted-by":"crossref","unstructured":"Huang X, Kwiatkowska M, Wang S, Wu M (2017) Safety verification of deep neural networks. In: Computer aided verification: 29th international conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30, pp 3\u201329. Springer","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"457_CR26","doi-asserted-by":"crossref","unstructured":"Katz G, Barrett C, Dill DL, Julian K, Kochenderfer MJ (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. In: International conference on computer aided verification, pp 97\u2013117. Springer","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"457_CR27","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Comput Aided Verif","author":"G Katz","year":"2019","unstructured":"Katz G, Huang DA, Ibeling D, Julian K, Lazarus C, Lim R, Shah P, Thakoor S, Wu H, Al Z, Dill DL, Kochenderfer MJ, Barrett C (2019) The marabou framework for verification and analysis of deep neural networks. In: Dillig I, Serdar T (eds) Comput Aided Verif. Springer, Cham, pp 443\u2013452"},{"key":"457_CR28","unstructured":"Khachiyan LG (1979), A polynomial time algorithm for linear programming. Doklady Akademii Nauk SSSR, 244(5), 1093\u20131096, English translation in Soviet Math. Dokl. 20:191\u2013194"},{"key":"457_CR29","first-page":"159","volume":"III","author":"F Klee","year":"1972","unstructured":"Klee F, Minty GJ (1972) How good is the simplex algorithm? Inequalities III:159\u2013175","journal-title":"Inequalities"},{"issue":"2","key":"457_CR30","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1109\/TITS.2019.2962338","volume":"22","author":"S Kuutti","year":"2020","unstructured":"Kuutti S, Bowden R, Jin Y, Barber P, Fallah S (2020) A survey of deep learning applications to autonomous vehicle control. IEEE Trans Intell Transp Syst 22(2):712\u2013733","journal-title":"IEEE Trans Intell Transp Syst"},{"key":"457_CR31","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/11559306_9","volume-title":"Frontiers of combining systems","author":"SK Lahiri","year":"2005","unstructured":"Lahiri SK, Musuvathi M (2005) An efficient decision procedure for UTVPI constraints. In: Gramlich B (ed) Frontiers of combining systems. Springer, Berlin, pp 168\u2013183"},{"key":"457_CR32","unstructured":"Liu C, Arnon T, Lazarus C, Barrett C, Kochenderfer MJ (2019). Algorithms for verifying deep neural networks. arXiv:1903.06758"},{"key":"457_CR33","doi-asserted-by":"crossref","unstructured":"Manzanas\u00a0Lopez D, Johnson T, Tran H-D, Bak S, Chen X, Hobbs KL (2021) Verification of neural network compression of ACAS Xu lookup tables with star set reachability. In: AIAA Scitech 2021 Forum, p 0995","DOI":"10.2514\/6.2021-0995"},{"issue":"1","key":"457_CR34","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 (2006) The octagon abstract domain. Higher-order Symb Comput 19(1):31\u2013100","journal-title":"Higher-order Symb Comput"},{"key":"457_CR35","unstructured":"Orlin JB (1996) A polynomial time primal network simplex algorithm for minimum cost flows. In: Proceedings of the 7th annual ACM-SIAM symposium on discrete algorithms, SODA \u201996, 474-481, USA. Society for Industrial and Applied Mathematics"},{"issue":"4","key":"457_CR36","first-page":"6","volume":"1","author":"G Singh","year":"2018","unstructured":"Singh G, Gehr T, Mirman M, P\u00fcschel M, Vechev MT (2018) Fast and effective robustness certification. NeurIPS 1(4):6","journal-title":"NeurIPS"},{"issue":"POPL","key":"457_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290354","volume":"3","author":"G Singh","year":"2019","unstructured":"Singh G, Gehr T, P\u00fcschel M, Vechev M (2019) An abstract domain for certifying neural networks. Proc ACM Program Lang 3(POPL):1\u201330","journal-title":"Proc ACM Program Lang"},{"key":"457_CR38","volume-title":"Reinforcement learning: an introduction","author":"RS Sutton","year":"2018","unstructured":"Sutton RS, Barto AG (2018) Reinforcement learning: an introduction, 2nd edn. MIT Press, Cambridge","edition":"2"},{"key":"457_CR39","unstructured":"Tjeng V, Xiao KY, Tedrake R (2018) Evaluating robustness of neural networks with mixed integer programming. In: International conference on learning representations"},{"key":"457_CR40","doi-asserted-by":"crossref","unstructured":"Tran H-D, Bak S, Xiang W, Johnson TT (2020). Verification of deep convolutional neural networks using imagestars. In: International conference on computer aided verification, pp 18\u201342. Springer","DOI":"10.1007\/978-3-030-53288-8_2"},{"issue":"5s","key":"457_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358230","volume":"18","author":"H-D Tran","year":"2019","unstructured":"Tran H-D, Cai F, Diego ML, Musau P, Johnson TT, Koutsoukos X (2019) Safety verification of cyber-physical systems with reinforcement learning control. ACM Trans Embed Comput Syst (TECS) 18(5s):1\u201322","journal-title":"ACM Trans Embed Comput Syst (TECS)"},{"key":"457_CR42","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","volume-title":"Formal methods\u2014the next 30 years","author":"H-D Tran","year":"2019","unstructured":"Tran H-D, Manzanas Lopez D, Musau P, Yang X, Nguyen LV, Xiang W, Johnson TT (2019) Star-based reachability analysis of deep neural networks. In: ter Beek MH, McIver A, Oliveira JN (eds) Formal methods\u2014the next 30 years. Springer, Cham, pp 670\u2013686"},{"key":"457_CR43","doi-asserted-by":"crossref","unstructured":"Tran H-D, Pal N, Musau P, Lopez DM, Hamilton N, Yang X, Bak S, Johnson TT (2021) Robustness verification of semantic segmentation neural networks using relaxed reachability. In: International conference on computer aided verification, pp 263\u2013286. Springer","DOI":"10.1007\/978-3-030-81685-8_12"},{"key":"457_CR44","doi-asserted-by":"crossref","unstructured":"Tran H-D, Yang X, Lopez DM, Musau P, Nguyen LV, Xiang W, Bak S, Johnson TT (2020) NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: International conference on computer aided verification, pp 3\u201317. Springer","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"457_CR45","unstructured":"Wang S, Pei K, Whitehouse J, Yang J, Jana S (2018) Efficient formal safety analysis of neural networks. In: Advances in neural information processing systems, vol 31"},{"key":"457_CR46","unstructured":"Wang S, Zhang H, Xu K, Lin X, Jana S, Hsieh C-J, Kolter JZ (2021) Beta-crown: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv:2103.06624"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00457-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00457-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00457-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T18:02:58Z","timestamp":1735408978000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00457-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,17]]},"references-count":46,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["457"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00457-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,17]]},"assertion":[{"value":"7 December 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 May 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"We declare that we have no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This manuscript was created by following all the ethical guidelines. In particular, an extended abstract of this work was published in FM 2023. This has been indicated in the abstract as a footnote.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}}]}}