{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:57Z","timestamp":1775873517125,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,6,9]],"date-time":"2014-06-09T00:00:00Z","timestamp":1402272000000},"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"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,6,9]]},"DOI":"10.1145\/2594291.2594301","type":"proceedings-article","created":{"date-parts":[[2014,5,13]],"date-time":"2014-05-13T08:18:34Z","timestamp":1399969114000},"page":"270-281","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["End-to-end verification of stack-space bounds for C programs"],"prefix":"10.1145","author":[{"given":"Quentin","family":"Carbonneaux","sequence":"first","affiliation":[{"name":"Yale University"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Yale University"}]},{"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[{"name":"Yale University"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University"}]}],"member":"320","published-online":{"date-parts":[[2014,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8_19"},{"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","volume-title":"Program Logics for Certified Compilers","author":"Appel A. W.","year":"2013","unstructured":"A. W. Appel Program Logics for Certified Compilers . Cambridge University Press , 2013 . A. W. Appel et al. Program Logics for Certified Compilers. Cambridge University Press, 2013."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.003"},{"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","volume-title":"Embedded Real Time Software and Systems (ERTS 2012)","author":"Bedin Fran\u00e7a R.","year":"2012","unstructured":"R. Bedin Fran\u00e7a , S. Blazy , D. Favre-Felix , X. Leroy , M. Pantel , and J. Souyris . Formally Verified Optimizing Compilation in ACG-based Flight Control Software . In Embedded Real Time Software and Systems (ERTS 2012) , 2012 . R. Bedin Fran\u00e7a, S. Blazy, D. Favre-Felix, X. Leroy, M. Pantel, and J. Souyris. Formally Verified Optimizing Compilation in ACG-based Flight Control Software. In Embedded Real Time Software and Systems (ERTS 2012), 2012."},{"key":"e_1_3_2_1_7_1","volume-title":"Conf. (VSTTE'13)","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'13) , 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'13), 2013. To appear."},{"key":"e_1_3_2_1_8_1","first-page":"47","volume-title":"Static Checking of Interrupt-Driven Software. In 23rd Int. Conf. on Soft. Engineering (ICSE'01)","author":"Brylow D.","year":"2001","unstructured":"D. Brylow , N. Damgaard , and J. Palsberg . Static Checking of Interrupt-Driven Software. In 23rd Int. Conf. on Soft. Engineering (ICSE'01) , pages 47 -- 56 , 2001 . D. Brylow, N. Damgaard, and J. Palsberg. Static Checking of Interrupt-Driven Software. In 23rd Int. Conf. on Soft. Engineering (ICSE'01), pages 47--56, 2001."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375656"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250742"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_3_2_1_13_1","unstructured":"Express Logic Inc. Helping you avoid stack overflow crashes! White Paper 2014. URL http:\/\/rtos.com\/images\/uploads\/Stack_Analysis_White_paper.1_.pdf.  Express Logic Inc. Helping you avoid stack overflow crashes! White Paper 2014. URL http:\/\/rtos.com\/images\/uploads\/Stack_Analysis_White_paper.1_.pdf."},{"key":"e_1_3_2_1_14_1","volume-title":"Static Memory and Timing Analysis of Embedded Systems Code. In 3rd Europ. Symp. on Verification and Validation of Software Systems (VVSS'07)","author":"Ferdinand C.","year":"2007","unstructured":"C. Ferdinand , R. Heckmann , and B. Franzen . Static Memory and Timing Analysis of Embedded Systems Code. In 3rd Europ. Symp. on Verification and Validation of Software Systems (VVSS'07) , 2007 . C. Ferdinand, R. Heckmann, and B. Franzen. Static Memory and Timing Analysis of Embedded Systems Code. In 3rd Europ. Symp. on Verification and Validation of Software Systems (VVSS'07), 2007."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103799.2103803"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1128020.1128563"},{"key":"e_1_3_2_1_18_1","first-page":"37","volume-title":"2nd Int. Conf. (GPCE'03)","author":"Hammond K.","year":"2003","unstructured":"K. Hammond and G. Michaelson . Hume: A Domain-Specific Language for Real-Time Embedded Systems. In Generative Progr. and Component Eng ., 2nd Int. Conf. (GPCE'03) , pages 37 -- 56 , 2003 . K. Hammond and G. Michaelson. Hume: A Domain-Specific Language for Real-Time Embedded Systems. In Generative Progr. and Component Eng., 2nd Int. Conf. (GPCE'03), pages 37--56, 2003."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.18"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.43"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113833"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1859204.1859226"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_36_1","volume-title":"Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symposium (SAS'11)","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'11) , 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'11), 2011."}],"event":{"name":"PLDI '14: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Edinburgh United Kingdom","acronym":"PLDI '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","NSF"]},"container-title":["Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2594291.2594301","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2594291.2594301","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:01:04Z","timestamp":1750215664000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2594291.2594301"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,9]]},"references-count":35,"alternative-id":["10.1145\/2594291.2594301","10.1145\/2594291"],"URL":"https:\/\/doi.org\/10.1145\/2594291.2594301","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2666356.2594301","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,6,9]]},"assertion":[{"value":"2014-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}