{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,27]],"date-time":"2026-10-27T19:49:40Z","timestamp":1793130580742,"version":"4.5.0"},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,11]]},"DOI":"10.1109\/fmcad.2009.5351120","type":"proceedings-article","created":{"date-parts":[[2009,12,11]],"date-time":"2009-12-11T13:55:16Z","timestamp":1260539716000},"page":"205-212","source":"Crossref","is-referenced-by-count":17,"title":["Finding heap-bounds for hardware synthesis"],"prefix":"10.1109","author":[{"given":"B.","family":"Cook","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A.","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Magill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A.","family":"Rybalchenko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J.","family":"Simsa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Singh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"V.","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1109\/54.587745"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.2003.1183177"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.87"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_24"},{"key":"34","year":"0"},{"key":"16","year":"0"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/FPGA.2000.903392"},{"key":"14","doi-asserted-by":"crossref","DOI":"10.1145\/1480881.1480898","article-title":"SPEED: Precise and efficient static estimation of program computational complexity","author":"gulwani","year":"2009","journal-title":"POPL"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"12","first-page":"1","article-title":"Uber die theorie der einfachen ungleichungen.","volume":"124","author":"farkas","year":"1902","journal-title":"J die Reine und Angewandte Math"},{"key":"21","year":"2008","journal-title":"CleanC analysis tools"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_3"},{"key":"22","year":"0"},{"key":"23","year":"0"},{"key":"24","year":"0"},{"key":"25","year":"0"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1220583"},{"key":"27","article-title":"A complete method for the synthesis of linear ranking functions","author":"podelski","year":"2004","journal-title":"VMCAI"},{"key":"28","article-title":"ARMC: The logical choice for software model checking with abstraction refinement","author":"podelski","year":"2007","journal-title":"PADL"},{"key":"29","article-title":"Automatic parallelization with separation logic","author":"raza","year":"2009","journal-title":"ESOP"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289440"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250769"},{"key":"10","article-title":"A local shape analysis based on separation logic","author":"distefano","year":"2006","journal-title":"TACAS"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/1296907.1296922"},{"key":"30","article-title":"SHard: A Scheme to hardware compiler","author":"saint-mleux","year":"2006","journal-title":"Workshop on Scheme and Functional Programming"},{"key":"7","article-title":"Impact of loop unrolling on throughput, area and clock frequency in ROCCC: C to VHDL compiler for FPGAs","author":"buyukkurt","year":"2006","journal-title":"Int Workshop On Applied Reconfigurable Computing"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253815"},{"key":"32","year":"0"},{"key":"5","article-title":"The FM9001 microprocessor proof","author":"brock","year":"1994"},{"key":"31","year":"0"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2006.5.5.a2"},{"key":"9","article-title":"Linear invariant generation using non-linear constraint solving","author":"colon","year":"2003","journal-title":"C AV"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"}],"event":{"name":"2009 Formal Methods in Computer-Aided Design (FMCAD)","location":"Austin, TX, USA","start":{"date-parts":[[2009,11,15]]},"end":{"date-parts":[[2009,11,18]]}},"container-title":["2009 Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5344684\/5351113\/05351120.pdf?arnumber=5351120","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,18]],"date-time":"2024-03-18T00:59:45Z","timestamp":1710723585000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5351120\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2009.5351120","relation":{},"subject":[],"published":{"date-parts":[[2009,11]]}}}