{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:54Z","timestamp":1780994634884,"version":"3.54.1"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["PhD Fellowship"],"award-info":[{"award-number":["PhD Fellowship"]}],"id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1942537"],"award-info":[{"award-number":["1942537"]}],"id":[{"id":"10.13039\/100000001","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":[[2024,1,2]]},"abstract":"<jats:p>\n            This paper presents a program analysis method that generates program summaries involving polynomial arithmetic. Our approach builds on prior techniques that use solvable polynomial maps for summarizing loops. These techniques are able to generate\n            <jats:italic toggle=\"yes\">all<\/jats:italic>\n            polynomial invariants for a restricted class of programs, but cannot be applied to programs outside of this class\u2014for instance, programs with nested loops, conditional branching, unstructured control flow, etc. There currently lacks approaches to apply these prior methods to the case of general programs. This paper bridges that gap. Instead of restricting the kinds of programs we can handle, our method\n            <jats:italic toggle=\"yes\">abstracts<\/jats:italic>\n            every loop into a model that can be solved with prior techniques, bringing to bear prior work on solvable polynomial maps to general programs. While no method can generate all polynomial invariants for arbitrary programs, our method establishes its merit through a\n            <jats:italic toggle=\"yes\">monotonicty<\/jats:italic>\n            result. We have implemented our techniques, and tested them on a suite of benchmarks from the literature. Our experiments indicate our techniques show promise on challenging verification tasks requiring non-linear reasoning.\n          <\/jats:p>","DOI":"10.1145\/3632867","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"724-752","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-6310-413X","authenticated-orcid":false,"given":"John","family":"Cyphert","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7294-9165","authenticated-orcid":false,"given":"Zachary","family":"Kincaid","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00121"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_3"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088216.1088219"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_7"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385969"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16721-3"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290358"},{"key":"e_1_3_1_10_1","doi-asserted-by":"crossref","unstructured":"John Cyphert and Zachary Kincaid. 2023a. Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis. arXiv:2311.04092","DOI":"10.1145\/3632867"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"John Cyphert and Zachary Kincaid. 2023b. Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis Artifact. https:\/\/doi.org\/10.5281\/zenodo.10069757 10.5281\/zenodo.10069757","DOI":"10.5281\/zenodo.10069757"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Jean-Charles Faug\u00e8re. 1999. A new efficient algorithm for computing Gr\u00f6bner bases (F4). Journal of Pure and Applied Algebra 139 1 (1999) 61\u201388. https:\/\/doi.org\/10.1016\/S0022-4049(99)00005-5 10.1016\/S0022-4049(99)00005-5","DOI":"10.1016\/S0022-4049(99)00005-5"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15582-6_17"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-65474-0_5"},{"key":"e_1_3_1_16_1","volume-title":"Algorithms Related to Multiplicative Representations of Algebraic Numbers","author":"Ge Guoqiang","year":"1993","unstructured":"Guoqiang Ge. 1993. Algorithms Related to Multiplicative Representations of Algebraic Numbers. Ph. D. Dissertation. Mathematics Department, University of California at Berkeley, Berkeley, CA."},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586052"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209142"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3614319"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2017.2690633"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.03.002"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571237"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_3"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.06.005"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2004. Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations. In Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (Santander Spain) (ISSAC \u201904). Association for Computing Machinery New York NY USA 266\u2013273. https:\/\/doi.org\/10.1145\/1005285.1005324 10.1145\/1005285.1005324","DOI":"10.1145\/1005285.1005324"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"e_1_3_1_36_1","unstructured":"The FLINT team. 2023. FLINT: Fast Library for Number Theory. Version 2.9.0 https:\/\/flintlib.org."},{"key":"e_1_3_1_37_1","article-title":"On combination of stochastic and deterministic processes","author":"Ulam S. M.","year":"1947","unstructured":"S. M. Ulam and John von Neumann. 1947. On combination of stochastic and deterministic processes. Summer meeting of the American Mathematical Society.","journal-title":"Summer meeting of the American Mathematical Society"},{"key":"e_1_3_1_38_1","unstructured":"Philipp Wendler and Dirk Beyer. 2023. Bench Exec 3.16. https:\/\/github.com\/sosy-lab\/benchexec."},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_3"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454110"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632867","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632867","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632867","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:02:36Z","timestamp":1751659356000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632867"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632867"],"URL":"https:\/\/doi.org\/10.1145\/3632867","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}