{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:14:34Z","timestamp":1784837674436,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T00:00:00Z","timestamp":1433289600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-10-2-0254, FA8750-12-2-0293"],"award-info":[{"award-number":["FA8750-10-2-0254, FA8750-12-2-0293"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1319671, 1065451"],"award-info":[{"award-number":["1319671, 1065451"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-12-1-0478"],"award-info":[{"award-number":["N00014-12-1-0478"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,6,3]]},"DOI":"10.1145\/2737924.2737955","type":"proceedings-article","created":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T11:35:56Z","timestamp":1433331356000},"page":"467-478","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":75,"title":["Compositional certified resource bounds"],"prefix":"10.1145","author":[{"given":"Quentin","family":"Carbonneaux","sequence":"first","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,6,3]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28872-2_10"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882102"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_27"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_1_7_1","volume-title":"System-Level Non-Interference for Constant-Time Cryptography. IACR Cryptology ePrint Archive","author":"Barthe G.","year":"2014","unstructured":"G. Barthe , G. Betarte , J. D. Campo , C. Luna , and D. Pichardie . System-Level Non-Interference for Constant-Time Cryptography. IACR Cryptology ePrint Archive , 2014 :422, 2014. G. Barthe, G. Betarte, J. D. Campo, C. Luna, and D. Pichardie. System-Level Non-Interference for Constant-Time Cryptography. IACR Cryptology ePrint Archive, 2014:422, 2014."},{"key":"e_1_3_2_1_8_1","first-page":"118","volume-title":"Conf. (LPAR\u201910)","author":"Blanc R.","year":"2010","unstructured":"R. Blanc , T. A. Henzinger , T. Hottelier , and L. Kov\u00e1cs . ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning - 16th Int . Conf. (LPAR\u201910) , pages 103\u2013 118 , 2010 . R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kov\u00e1cs. ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning - 16th Int. Conf. (LPAR\u201910), pages 103\u2013118, 2010."},{"key":"e_1_3_2_1_9_1","volume-title":"Conf. (VSTTE\u201913)","author":"Blazy S.","year":"2013","unstructured":"S. Blazy , A. Maroneze , and D. Pichardie . Formal Verification of Loop Bound Estimation for WCET Analysis. In Verified Software: Theories, Tools, Experiments - 5th Int . Conf. (VSTTE\u201913) , 2013 . To appear. S. Blazy, A. Maroneze, and D. Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. In Verified Software: Theories, Tools, Experiments - 5th Int. Conf. (VSTTE\u201913), 2013. To appear."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375655"},{"key":"e_1_3_2_1_11_1","first-page":"155","volume-title":"Conf. (TACAS\u201914)","author":"Brockschmidt M.","year":"2014","unstructured":"M. Brockschmidt , F. Emmes , S. Falke , C. Fuhs , and J. Giesl . Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Alg. for the Constr. and Anal. of Systems - 20th Int . Conf. (TACAS\u201914) , pages 140\u2013 155 , 2014 . M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Alg. for the Constr. and Anal. of Systems - 20th Int. Conf. (TACAS\u201914), pages 140\u2013155, 2014."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509546"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594301"},{"key":"e_1_3_2_1_15_1","volume-title":"USENIX Annual Technical Conference (USENIX\u201910)","author":"Carroll A.","year":"2010","unstructured":"A. Carroll and G. Heiser . An Analysis of Power Consumption in a Smartphone . In USENIX Annual Technical Conference (USENIX\u201910) , 2010 . A. Carroll and G. Heiser. An Analysis of Power Consumption in a Smartphone. In USENIX Annual Technical Conference (USENIX\u201910), 2010."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384676"},{"key":"e_1_3_2_1_17_1","volume-title":"https: \/\/projects.coin-or.org\/Clp","author":"Project OR","year":"2014","unstructured":"COIN- OR Project . CLP (Coin-or Linear Programming). https: \/\/projects.coin-or.org\/Clp , 2014 . Accessed : 2014-11-12. COIN-OR Project. CLP (Coin-or Linear Programming). https: \/\/projects.coin-or.org\/Clp, 2014. Accessed: 2014-11-12."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806630"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_3_2_1_22_1","volume-title":"Type-Based Amortized Resource Analysis with Integers and Arrays. In 12th International Symposium on Functional and Logic Programming (FLOPS\u201914)","author":"Hoffmann J.","year":"2014","unstructured":"J. Hoffmann and Z. Shao . Type-Based Amortized Resource Analysis with Integers and Arrays. In 12th International Symposium on Functional and Logic Programming (FLOPS\u201914) , 2014 . J. Hoffmann and Z. Shao. Type-Based Amortized Resource Analysis with Integers and Arrays. In 12th International Symposium on Functional and Logic Programming (FLOPS\u201914), 2014."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_3"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_19"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04138-9_1"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113833"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_3_2_1_33_1","volume-title":"Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symposium (SAS\u201911)","author":"Zuleger F.","year":"2011","unstructured":"F. Zuleger , M. Sinn , S. Gulwani , and H. Veith . Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symposium (SAS\u201911) , 2011 . F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symposium (SAS\u201911), 2011."}],"event":{"name":"PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Portland OR USA","acronym":"PLDI '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2737924.2737955","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2737924.2737955","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:12:23Z","timestamp":1750212743000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2737924.2737955"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,3]]},"references-count":32,"alternative-id":["10.1145\/2737924.2737955","10.1145\/2737924"],"URL":"https:\/\/doi.org\/10.1145\/2737924.2737955","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2813885.2737955","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,6,3]]},"assertion":[{"value":"2015-06-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}