{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:17:04Z","timestamp":1763968624521,"version":"build-2065373602"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF 1900924, CCF 1901069, CCF 2007428"],"award-info":[{"award-number":["CCF 1900924, CCF 1901069, CCF 2007428"]}],"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":[[2025,4,9]]},"abstract":"<jats:p>Many synthesis and verification problems can be reduced to determining the truth of formulas over the real numbers. These formulas often involve constraints with integrals in them. To this end, we extend the framework of \u03b4-decision procedures with techniques for handling integrals of user-specified real functions. We implement this decision procedure in the tool \u222bdReal, which is built on top of dReal. We evaluate \u222bdReal on a suite of problems that include formulas verifying the fairness of algorithms and the privacy and the utility of privacy mechanisms and formulas that synthesize parameters for the desired utility of privacy mechanisms. The performance of the tool in these experiments demonstrates the effectiveness of \u222bdReal.<\/jats:p>","DOI":"10.1145\/3720446","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"704-729","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Checking \u03b4-Satisfiability of Reals with Integrals"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7824-4054","authenticated-orcid":false,"given":"Cody","family":"Rivera","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7522-5878","authenticated-orcid":false,"given":"Bishnu","family":"Bhusal","sequence":"additional","affiliation":[{"name":"University of Missouri, Columbia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1674-1650","authenticated-orcid":false,"given":"Rohit","family":"Chadha","sequence":"additional","affiliation":[{"name":"University of Missouri, Columbia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8331-7912","authenticated-orcid":false,"given":"A. Prasad","family":"Sistla","sequence":"additional","affiliation":[{"name":"University of Illinois at Chicago, Chicago, USA"},{"name":"Discovery Partners Institute, Chicago, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7977-0080","authenticated-orcid":false,"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Accessed 2023. DReal4. https:\/\/github.com\/dreal\/dreal4"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133904"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434289"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","unstructured":"Fr\u00e9d\u00e9ric Benhamou and Laurent Granvilliers. 2006. Chapter 16 - Continuous and Interval Constraints. In Handbook of Constraint Programming Francesca Rossi Peter van Beek and Toby Walsh (Eds.) (Foundations of Artificial Intelligence Vol. 2). Elsevier 571\u2013603. issn:1574-6526 https:\/\/doi.org\/10.1016\/S1574-6526(06)80020-9 10.1016\/S1574-6526(06)80020-9","DOI":"10.1016\/S1574-6526(06)80020-9"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623170"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_1"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536414.1536467"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_13"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679398"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_2_2_15_1","unstructured":"Ibex Team. Accessed 2023. Ibex Library. https:\/\/ibex-team.github.io\/ibex-lib\/"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2576802.2576828"},{"key":"e_1_2_2_17_1","unstructured":"Fredrik Johansson. 2017. New rigorous numerical integration in Arb. https:\/\/fredrikj.net\/blog\/2017\/11\/new-rigorous-numerical-integration-in-arb\/"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-6802-1"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_15"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.14778\/3055330.3055331"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_37"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14593603"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14948095"},{"key":"e_1_2_2_25_1","volume-title":"Real analysis","author":"Royden Halsey L.","unstructured":"Halsey L. Royden. 1988. Real analysis (3rd ed.). Macmillan, New York.","edition":"3"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/4304.003.0024"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/060659831"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23401-4_3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720446","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720446","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:09:30Z","timestamp":1760029770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720446"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":28,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720446"],"URL":"https:\/\/doi.org\/10.1145\/3720446","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}