{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:50Z","timestamp":1787592290104,"version":"build-2736575974"},"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\/legalcode"}],"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>\n                    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\n                    <jats:italic toggle=\"yes\">\u03b4<\/jats:italic>\n                    -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.\n                  <\/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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"Accessed 2023. DReal4. https:\/\/github.com\/dreal\/dreal4."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133904"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434289"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(06)80020-9"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623170"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_1"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Cynthia Dwork Moni Naor Omer Reingold Guy N Rothblum and Salil Vadhan. 2009. On the complexity of differentially private data release: efficient algorithms and hardness results. In Proceedings of the forty-first annual ACM symposium on Theory of computing. 381\u2013390. https:\/\/doi.org\/10.1145\/1536414.1536467 10.1145\/1536414.1536467","DOI":"10.1145\/1536414.1536467"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"A. Eggers N. Ramdani N. Nedialkov and M. Fr\u00e4nzle. 2011. Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods. In Proceedings of the International Conference on Software Engineering and Formal Methods. 172\u2013187. https:\/\/doi.org\/10.1007\/978-3-642-24690-6_13 10.1007\/978-3-642-24690-6_13","DOI":"10.1007\/978-3-642-24690-6_13"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Sicun Gao Soonho Kong and Edmund M. Clarke. 2013. Satisfiability modulo ODEs. In 2013 Formal Methods in Computer-Aided Design. 105\u2013112. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679398 10.1109\/FMCAD.2013.6679398","DOI":"10.1109\/FMCAD.2013.6679398"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_2_16_2","unstructured":"Ibex Team. Accessed 2023. Ibex Library. https:\/\/ibex-team.github.io\/ibex-lib\/."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/2576802.2576828"},{"key":"e_1_3_2_18_2","unstructured":"Fredrik Johansson. 2017. New rigorous numerical integration in Arb. https:\/\/fredrikj.net\/blog\/2017\/11\/new-rigorousnumerical-integration-in-arb\/."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-6802-1"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Soonho Kong Sicun Gao Wei Chen and Edmund M. Clarke. 2015. dReach: \u03b4-Reachability Analysis for Hybrid Systems. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference TACAS 2015 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2015 London UK April 11-18 2015. Proceedings. 200\u2013205. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_15 10.1007\/978-3-662-46681-0_15","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_15"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.14778\/3055330.3055331"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_37"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Cody Rivera Bishnu Bhusal Rohit Chadha Aravinda Prasad Sistla and Mahesh Viswanathan. 2025. Artifact for Paper Submission \"Checking \u03b4-Satisfiability of Reals with Integrals (v1)\". https:\/\/doi.org\/10.5281\/zenodo.14593603 10.5281\/zenodo.14593603","DOI":"10.5281\/zenodo.14593603"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Cody Rivera Bishnu Bhusal Rohit Chadha Aravinda Prasad Sistla and Mahesh Viswanathan. 2025. Artifact for Paper Submission \"Checking \u03b4-Satisfiability of Reals with Integrals (v2)\". https:\/\/doi.org\/10.5281\/zenodo.14948095 10.5281\/zenodo.14948095","DOI":"10.5281\/zenodo.14948095"},{"key":"e_1_3_2_26_2","volume-title":"Real analysis","author":"Royden Halsey L.","year":"1988","unstructured":"Halsey L. Royden. 1988. Real analysis (3rd ed.). Macmillan, New York.","edition":"3"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Danny De Schreye. 1999. Revising hull and box consistency. In Logic Programming: Proceedings of the 1999 International Conference on Logic Programming. 230\u2013244. https:\/\/doi.org\/10.7551\/mitpress\/4304.003.0024 10.7551\/mitpress\/4304.003.0024","DOI":"10.7551\/mitpress\/4304.003.0024"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1137\/060659831"},{"key":"e_1_3_2_29_2","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":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720446","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:29:55Z","timestamp":1787588995000},"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":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}