{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:21:53Z","timestamp":1760059313481,"version":"build-2065373602"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Datalog engines for fixpoint evaluation have brought great benefits to static program analysis over the past decades. A Datalog specification of an analysis allows a declarative, easy-to-maintain specification, without sacrificing performance, and indeed often achieving significant speedups compared to hand-coded algorithms.<\/jats:p>\n          <jats:p>\n            However, these benefits come with a certain loss of control. Datalog evaluation is bottom-up, meaning that all inferences (from a set of initial facts) are performed and\n            <jats:italic toggle=\"yes\">all<\/jats:italic>\n            their conclusions are outputs of the computation. In practice, virtually every program analysis expressed in Datalog becomes unscalable for some inputs, due to the worst-case blowup of computing all results, even when a partial answer would have been perfectly satisfactory.\n          <\/jats:p>\n          <jats:p>\n            In this work, we present a simple, uniform, and elegant solution to the problem, with great practical effectiveness and application to virtually any Datalog-based analysis. The approach consists of leveraging the\n            <jats:italic toggle=\"yes\">choice<\/jats:italic>\n            construct, supported natively in modern Datalog engines like Souffle. The choice construct allows the definition of functional dependencies in a relation and has been used in the past for expressing worklist algorithms. We show a near-universal construction that allows the choice construct to flexibly limit evaluation of predicates. The technique is applicable to practically any analysis architecture imaginable, since it adaptively prunes evaluation results when a (programmer-controlled) projection of a relation exceeds a desired cardinality.\n          <\/jats:p>\n          <jats:p>We apply the technique to probably the largest, pre-existing Datalog analysis frameworks in existence: Doop (for Java bytecode) and the main client analyses from the Gigahorse framework (for Ethereum smart contracts). Without needing to understand the existing analysis logic and with minimal, local-only changes, the performance of each framework increases dramatically, by over 20x for the hardest inputs, with near-negligible sacrifice in completeness.<\/jats:p>","DOI":"10.1145\/3763129","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"2199-2226","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-1605-967X","authenticated-orcid":false,"given":"Anastasios","family":"Antoniadis","sequence":"first","affiliation":[{"name":"University of Athens, Athens, Greece"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1788-053X","authenticated-orcid":false,"given":"Ilias","family":"Tsatiris","sequence":"additional","affiliation":[{"name":"Dedaub, Athens, Greece"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6790-2872","authenticated-orcid":false,"given":"Neville","family":"Grech","sequence":"additional","affiliation":[{"name":"University of Malta, Msida, Malta"},{"name":"Dedaub, San Gwann, Malta"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0499-0182","authenticated-orcid":false,"given":"Yannis","family":"Smaragdakis","sequence":"additional","affiliation":[{"name":"University of Athens, Athens, Greece"},{"name":"Dedaub, Athens, Greece"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"volume-title":"Program Analysis and Specialization for the C Programming Language. Ph. D. Dissertation. DIKU","author":"Andersen Lars O.","key":"e_1_2_1_1_1","unstructured":"Lars O. Andersen. 1994. Program Analysis and Specialization for the C Programming Language. Ph. D. Dissertation. DIKU, University of Copenhagen."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386026"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15723754"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2147769.2147770"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640108"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2024.10"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55015-1_7"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00120"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2018.26"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133926"},{"key":"e_1_2_1_13_1","unstructured":"Sergio Greco and Carlo Zaniolo. 1998. Greedy Algorithms in Datalog with Choice and Negation. In IJCSLP. https:\/\/api.semanticscholar.org\/CorpusID:15290518"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378802"},{"volume-title":"Programming Languages and Systems","author":"Hu Xiaowen","key":"e_1_2_1_15_1","unstructured":"Xiaowen Hu, Joshua Karp, David Zhao, Abdul Zreika, Xi Wu, and Bernhard Scholz. 2021. The Choice Construct in the Souffl\u00e9 Language. In Programming Languages and Systems, Hakjoo Oh (Ed.). Springer International Publishing, Cham. 163\u2013181. isbn:978-3-030-89051-3"},{"key":"e_1_2_1_16_1","first-page":"2003","article-title":"Information Technology\u2014Database Languages\u2014SQL\u2014Part 2: Foundation (SQL\/Foundation)","volume":"9075","author":"IEC.","year":"2003","unstructured":"ISO\/IEC. 2003. Information Technology\u2014Database Languages\u2014SQL\u2014Part 2: Foundation (SQL\/Foundation). International Standard ISO\/IEC 9075-2:2003.","journal-title":"International Standard ISO\/IEC"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276510"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498720"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133924"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462191"},{"volume-title":"Proceedings of the Workrhop on Logical Bases for Data Bases.","author":"Kunifuji S.","key":"e_1_2_1_21_1","unstructured":"S. Kunifuji and H. Yokota. 1982. Prolog and Relational Databases for 5th Generation Computer Systems. In Proceedings of the Workrhop on Logical Bases for Data Bases."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065167.1065169"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236041"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3381915"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2644805"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_11"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591242"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213847"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491417"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_2_1_31_1","unstructured":"Chris Martens Robert J. Simmons and Michael Arntzenius. 2024. Finite-Choice Logic Programming. arxiv:2405.19040. arxiv:2405.19040"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434315"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1044834.1044835"},{"key":"e_1_2_1_34_1","volume-title":"Chord: A Versatile Platform for Program Analysis. In 2011 ACM SIGPLAN Conf. on Programming Language Design and Implementation. Tutorial","author":"Naik Mayur","year":"2011","unstructured":"Mayur Naik. 2011. Chord: A Versatile Platform for Program Analysis. In 2011 ACM SIGPLAN Conf. on Programming Language Design and Implementation. Tutorial"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594318"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2259016.2259050"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/93597.93621"},{"volume-title":"Using Datalog for Fast and Easy Program Analysis","author":"Smaragdakis Yannis","key":"e_1_2_1_39_1","unstructured":"Yannis Smaragdakis and Martin Bravenboer. 2011. Using Datalog for Fast and Easy Program Analysis. In Datalog Reloaded, Oege de Moor, Georg Gottlob, Tim Furche, and Andrew Sellers (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 245\u2013251. isbn:978-3-642-24206-9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926390"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485540"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594320"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.22"},{"key":"e_1_2_1_44_1","first-page":"0362","volume-title":"Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation. 387\u2013400","author":"Sridharan Manu","year":"2006","unstructured":"Manu Sridharan and Rastislav Bodik. 2006. Refinement-based context-sensitive points-to analysis for Java. In PLDI \u201906: Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation. 387\u2013400. issn:0362-1340"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_15"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094817"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950296"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276509"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454026"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485524"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 12th International Conference on Very Large Data Bases (VLDB \u201986)","author":"Tsur Shalom","year":"1986","unstructured":"Shalom Tsur and Carlo Zaniolo. 1986. LDL: A Logic-Based Data Language. In Proceedings of the 12th International Conference on Very Large Data Bases (VLDB \u201986). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. 33\u201341. isbn:0934613184"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510046"},{"key":"e_1_2_1_53_1","unstructured":"Raf Venken. 1984. lhe Interaction between Prolog and Relational Databases. Internal Report BIM-prolog IR6.."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037744"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_8"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656417"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001440"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594327"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328464"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763129","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:48:57Z","timestamp":1760032137000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763129"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":59,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763129"],"URL":"https:\/\/doi.org\/10.1145\/3763129","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}