{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:16Z","timestamp":1750309516698,"version":"3.41.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T00:00:00Z","timestamp":1740268800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Spanish MCI, AEI and FEDER (EU) project","award":["PID2021-122830OB-C41"],"award-info":[{"award-number":["PID2021-122830OB-C41"]}]},{"name":"UCM","award":["CT42\/18-CT43\/18"],"award-info":[{"award-number":["CT42\/18-CT43\/18"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>\n            A program containing placeholders for unspecified statements or expressions is called an abstract (or schematic) program. Placeholder symbols occur naturally in program transformation rules, as used in refactoring, compilation or optimization. Static cost analysis derives the\n            <jats:italic>precise<\/jats:italic>\n            cost\u2014or\n            <jats:italic>upper<\/jats:italic>\n            and\n            <jats:italic>lower<\/jats:italic>\n            bounds for it\u2014of executing programs, as functions in terms of the program's input data size. We present a generalization of automated cost analysis that can handle abstract programs and, hence, can analyze the impact on the\n            <jats:italic>cost effect of program transformations<\/jats:italic>\n            . This kind of relational property requires provably precise cost bounds which are not always produced by cost analysis. Therefore, we certify by deductive verification that the inferred abstract cost bounds are correct and sufficiently precise. It is the first approach solving this problem. Both, abstract cost analysis and certification, are based on quantitative abstract execution (QAE) which in turn is a variation of abstract execution, a recently developed symbolic execution technique for abstract programs. To realize QAE the new concept of a cost invariant is introduced. QAE is implemented and runs fully automatically on a benchmark set consisting of representative optimization rules.\n          <\/jats:p>","DOI":"10.1145\/3705298","type":"journal-article","created":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T18:11:23Z","timestamp":1732212683000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Certified Cost Bounds for Abstract Programs"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0048-0705","authenticated-orcid":false,"given":"Elvira","family":"Albert","sequence":"first","affiliation":[{"name":"Complutense University of Madrid, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8000-7613","authenticated-orcid":false,"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[{"name":"Technical University Darmstadt, Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6219-1808","authenticated-orcid":false,"given":"Alicia","family":"Merayo","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4439-7129","authenticated-orcid":false,"given":"Dominic","family":"Steinh\u00f6fel","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,2,23]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/6448"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_21"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_12"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-015-0476-y"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_40"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499943"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71500-7_2"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.03.003"},{"key":"e_1_3_2_13_2","first-page":"200","volume-title":"Proceedings of the 17th International Symposium on Formal Methods","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe, Juan Manuel Crespo, and C\u00e9sar Kunz. 2011. Relational verification using product programs. In Proceedings of the 17th International Symposium on Formal Methods. Michael J. Butler and Wolfram Schulte (Eds.), Lecture Notes in Computer Science, Vol. 6664, Springer, 200\u2013214."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98047-8_3"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_7"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.3390\/electronics10182233"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_7"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/390016.808445"},{"issue":"4","key":"e_1_3_2_20_2","first-page":"13:1","article-title":"Analyzing runtime and size complexity of integer programs","volume":"38","author":"Brockschmidt Marc","year":"2016","unstructured":"Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and J\u00fcrgen Giesl. 2016. Analyzing runtime and size complexity of integer programs. ACM Transactions on Programming Languages and Systems 38, 4 (2016), 13:1\u201313:50. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=2866575","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_13"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.11.015"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_3_2_25_2","first-page":"193","volume-title":"Proceedings of the 2nd International Conference on Security in Pervasive Computing","volume":"3450","author":"Darvas \u00c1d\u00e1m","year":"2005","unstructured":"\u00c1d\u00e1m Darvas, Reiner H\u00e4hnle, and Dave Sands. 2005. A theorem proving approach to analysis of secure information flow. In Proceedings of the 2nd International Conference on Security in Pervasive Computing. Dieter Hutter and Markus Ullmann (Eds.), Lecture Notes in Computer Science, Vol. 3450, Springer, 193\u2013209. Retrieved from http:\/\/www.springerlink.com\/link.asp?id=rdqa8ejctda3yw64"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/4283.003.0035"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6\u02d916"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"e_1_3_2_30_2","volume-title":"Refactoring: Improving the Design of Existing Code","author":"Fowler Martin","year":"1999","unstructured":"Martin Fowler. 1999. Refactoring: Improving the Design of Existing Code. Addison-Wesley. With contributions by Kent Beck, John Brant, Willima Opdyke, and Don Roberts."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3410331"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1472"},{"key":"e_1_3_2_34_2","unstructured":"Neville Grech Kyriakos Georgiou James Pallister Steve Kerrison and Kerstin Eder. 2014. Static energy consumption analysis of LLVM IR programs. arXiv:1405.4565. Retrieved from http:\/\/arxiv.org\/abs\/1405.4565"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61470-6?8"},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science: State of the Art and Perspectives","author":"H\u00e4hnle Reiner","year":"2019","unstructured":"Reiner H\u00e4hnle and Marieke Huisman. 2019. Deductive verification: From pen-and-paper proofs to industrial tools. In Computing and Software Science: State of the Art and Perspectives. Bernhard Steffen and Gerhard Woeginger (Eds.), Lecture Notes in Computer Science, Vol. 10000. Springer, Cham, 345\u2013373."},{"key":"e_1_3_2_38_2","first-page":"424","volume-title":"Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","volume":"11244","author":"H\u00e4hnle Reiner","year":"2018","unstructured":"Reiner H\u00e4hnle and Dominic Steinh\u00f6fel. 2018. Modular, correct compilation with automatic soundness proofs. In Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. Tiziana Margaria and Bernhard Steffen (Eds.), Lecture Notes in Computer Science, Vol. 11244, Springer, 424\u2013447."},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0152-5"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_43_2","first-page":"327","volume-title":"Proceedings of the International Conference on Programming Language Design and Implementation (PLDI \u201909)","author":"Kundu Sudipta","year":"2009","unstructured":"Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. 2009. Proving optimizations correct using parameterized program equivalence. In Proceedings of the International Conference on Programming Language Design and Implementation (PLDI \u201909), 327\u2013337."},{"key":"e_1_3_2_44_2","unstructured":"Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel M. Zimmerman and Werner Dietl. 2013. JML Reference Manual. Retrieved from http:\/\/www.eecs.ucf.edu\/leavens\/JML\/\/OldReleases\/jmlrefman.pdf Draft revision 2344."},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3472456.3472521"},{"key":"e_1_3_2_46_2","first-page":"348","volume-title":"Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR \u201916)","volume":"6355","author":"Leino Rustan","year":"2010","unstructured":"Rustan Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR \u201916). E. M. Clarke and A. Voronkov (Eds.), Lecture Notes in Computer Science, Vol. 6355, Springer, Berlin, 348\u2013370. Retrieved from https:\/\/www.microsoft.com\/en-us\/research\/publication\/dafny-automatic-program-verifier-functional-correctness-2\/"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46559-3_5"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3166064"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015471"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78743-3_19"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709095"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64437-6_16"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_20"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.25534\/tuprints-00008540"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_28"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/361002.361016"},{"key":"e_1_3_2_59_2","volume-title":"Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction","author":"Wei\u00df Benjamin","year":"2011","unstructured":"Benjamin Wei\u00df. 2011. Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. Ph.D. Dissertation. Karlsruhe Institute of Technology. Retrieved from https:\/\/d-nb.info\/1010034960"},{"key":"e_1_3_2_60_2","doi-asserted-by":"crossref","unstructured":"Florian Zuleger Sumit Gulwani Moritz Sinn and Helmut Veith. 2012. Bound analysis of imperative programs with the size-change abstraction (extended version). arXiv:1203.5303. Retrieved from http:\/\/arxiv.org\/abs\/1203.5303","DOI":"10.1007\/978-3-642-23702-7_22"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3705298","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3705298","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:02Z","timestamp":1750295882000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3705298"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,23]]},"references-count":59,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3705298"],"URL":"https:\/\/doi.org\/10.1145\/3705298","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2025,2,23]]},"assertion":[{"value":"2022-02-02","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-11","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-23","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}