{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T02:50:10Z","timestamp":1784775010629,"version":"3.55.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["163117"],"award-info":[{"award-number":["163117"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>Numerical abstract domains such as Polyhedra, Octahedron, Octagon, Interval, and others are an essential component of static program analysis. The choice of domain offers a performance\/precision tradeoff ranging from cheap and imprecise (Interval) to expensive and precise (Polyhedra). Recently, significant speedups were achieved for Octagon and Polyhedra by manually decomposing their transformers to work with the Cartesian product of projections associated with partitions of the variable set. While practically useful, this manual process is time consuming, error-prone, and has to be applied from scratch for every domain.<\/jats:p>\n          <jats:p>In this paper, we present a generic approach for decomposing the transformers of sub-polyhedra domains along with conditions for checking whether the decomposed transformers lose precision with respect to the original transformers. These conditions are satisfied by most practical transformers, thus our approach is suitable for increasing the performance of these transformers without compromising their precision. Furthermore, our approach is ``black box:'' it does not require changes to the internals of the original non-decomposed transformers or additional manual effort per domain.<\/jats:p>\n          <jats:p>We implemented our approach and applied it to the domains of Zones, Octagon, and Polyhedra. We then compared the performance of the decomposed transformers obtained with our generic method versus the state of the art: the (non-decomposed) PPL for Polyhedra and the much faster ELINA (which uses manual decomposition) for Polyhedra and Octagon. Against ELINA we demonstrate finer partitions and an associated speedup of about 2x on average. Our results indicate that the general construction presented in this work is a viable method for improving the performance of sub-polyhedra domains. It enables designers of abstract domains to benefit from decomposition without re-writing all of their transformers from scratch as required by prior work.<\/jats:p>","DOI":"10.1145\/3158143","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["A practical construction for decomposing numerical abstract domains"],"prefix":"10.1145","volume":"2","author":[{"given":"Gagandeep","family":"Singh","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Markus","family":"P\u00fcschel","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"ELINA\n  : ETH Library for Numerical Analysis. http:\/\/elina.ethz.ch.  ELINA: ETH Library for Numerical Analysis. http:\/\/elina.ethz.ch."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0041-5553(68)90115-8"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.009"},{"key":"e_1_2_2_7_1","first-page":"130","volume-title":"Proc. International Symposium on Programming","author":"Cousot P.","year":"1976","unstructured":"P. Cousot and R. Cousot . Static determination of dynamic properties of programs . In Proc. International Symposium on Programming , pages 106\u2013 130 , 1976 . P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. International Symposium on Programming, pages 106\u2013130, 1976."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"issue":"1","key":"e_1_2_2_9_1","first-page":"28","article-title":"Precise widening operators for convex polyhedra","volume":"58","author":"Cousot R.","year":"2005","unstructured":"R. Cousot , R. Bagnara , P. M. Hill , E. Ricci , and E. Zaffanella . Precise widening operators for convex polyhedra . Science of Computer Programming , 58 ( 1 ): 28 \u2013 56 , 2005 . R. Cousot, R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Science of Computer Programming, 58(1):28 \u2013 56, 2005.","journal-title":"Science of Computer Programming"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449955.1449791"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_10"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_20"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0013-2"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_12"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_23"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2017.02.004"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1363686.1363736"},{"key":"e_1_2_2_21_1","first-page":"129","volume-title":"Principles and Practice of Constraint Programming","author":"Imbert J.","year":"1993","unstructured":"J. louis Imbert . Fourier\u2019s elimination : Which to choose ? Principles and Practice of Constraint Programming , pages 117\u2013 129 , 1993 . J. louis Imbert. Fourier\u2019s elimination: Which to choose? Principles and Practice of Constraint Programming, pages 117\u2013129, 1993."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_20"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_11"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45789-5_11"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.09.011"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_3"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_23"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-010-9062-8"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738000"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996869"},{"key":"e_1_2_2_33_1","volume-title":"A note on Chernikova\u2019s algorithm. Technical report","author":"Verge H. L.","year":"1994","unstructured":"H. L. Verge . A note on Chernikova\u2019s algorithm. Technical report , 1994 . H. L. Verge. A note on Chernikova\u2019s algorithm. Technical report, 1994."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158143","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158143","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158143"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158143"],"URL":"https:\/\/doi.org\/10.1145\/3158143","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}