{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:08:14Z","timestamp":1784200094641,"version":"3.55.0"},"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 Souffl\u00e9. 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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1788-053X","authenticated-orcid":false,"given":"Ilias","family":"Tsatiris","sequence":"additional","affiliation":[{"name":"Dedaub, Athens, Greece"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","volume-title":"Program Analysis and Specialization for the C Programming Language","author":"Andersen Lars O.","year":"1994","unstructured":"Lars O. Andersen. 1994. Program Analysis and Specialization for the C Programming Language. Ph. D. Dissertation.DIKU, University of Copenhagen."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386026"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Anastasios Antoniadis Ilias Tsatiris Neville Grech and Yannis Smaragdakis. 2025. Artifact: Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning). https:\/\/doi.org\/10.5281\/zenodo.15723754 10.5281\/zenodo.15723754","DOI":"10.5281\/zenodo.15723754"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2147769.2147770"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_3_1_7_2","doi-asserted-by":"crossref","unstructured":"Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly Declarative Specification of Sophisticated Points-to Analyses. In OOPSLA \u201909: Proceedings of the 24th annual ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications.","DOI":"10.1145\/1640089.1640108"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2024.10"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55015-l_7"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00120"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2018.26"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133926"},{"key":"e_1_3_1_14_2","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_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378802"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_10"},{"key":"e_1_3_1_17_2","unstructured":"ISO\/IEC. 2003. Information Technology\u2014Database Languages\u2014SQL\u2014Part 2: Foundation (SQL\/Foundation). International Standard ISO\/IEC 9075-2:2003."},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276510"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498720"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133924"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462191"},{"key":"e_1_3_1_22_2","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_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1065167.1065169"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236041"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3381915"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2644805"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_11"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591242"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213847"},{"key":"e_1_3_1_30_2","doi-asserted-by":"crossref","unstructured":"Magnus Madsen Benjamin Livshits and Michael Fanning. 2013. Practical Static Analysis of JavaScript Applications in the Presence of Frameworks and Libraries. In Proceedings of the ACM SIGSOFT International Symposium on the Foundations of Software Engineering.","DOI":"10.1145\/2491411.2491417"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_3_1_32_2","unstructured":"Chris Martens Robert J. Simmons and Michael Arntzenius. 2024. Finite-Choice Logic Programming.arXiv:2405.19040 [cs.PL] https:\/\/arxiv.org\/abs\/2405.19040."},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434315"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1044834.1044835"},{"key":"e_1_3_1_35_2","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_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594318"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2259016.2259050"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/93597.93621"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24206-9_14"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926390"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485540"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","unstructured":"Yannis Smaragdakis George Kastrinis and George Balatsouras. 2014. Introspective analysis: context-sensitivity across the board. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (Edinburgh United Kingdom) (PLDI \u201914). Association for Computing Machinery New York NY USA 485\u2013495.https:\/\/doi.org\/10.1145\/2594291.2594320 10.1145\/2594291.2594320","DOI":"10.1145\/2594291.2594320"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","unstructured":"Johannes Sp\u00e4th Lisa Nguyen Quang Do Karim Ali and Eric Bodden. 2016. Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java. In 30th European Conference on Object-Oriented Programming ECOOP 2016 July 18-22 2016 Rome Italy. 22:1\u201322:26.https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2016.22 10.4230\/LIPIcs.ECOOP.2016.22","DOI":"10.4230\/LIPIcs.ECOOP.2016.22"},{"key":"e_1_3_1_45_2","doi-asserted-by":"crossref","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.","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_15"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094817"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950296"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276509"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454026"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485524"},{"key":"e_1_3_1_52_2","first-page":"33","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."},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510046"},{"key":"e_1_3_1_54_2","unstructured":"Raf Venken. 1984. The Interaction between Prolog and Relational Databases. Technical Report. Internal Report BIM-prolog IR6."},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037744"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_8"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656417"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001440"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594327"},{"key":"e_1_3_1_60_2","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":[[2026,7,16]],"date-time":"2026-07-16T10:09:12Z","timestamp":1784196552000},"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":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}