{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T16:07:10Z","timestamp":1729613230401,"version":"3.28.0"},"reference-count":33,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1109\/rtas.2013.6531083","type":"proceedings-article","created":{"date-parts":[[2013,6,25]],"date-time":"2013-06-25T18:55:18Z","timestamp":1372186518000},"page":"97-106","source":"Crossref","is-referenced-by-count":10,"title":["Sequoll: A framework for model checking binaries"],"prefix":"10.1109","author":[{"given":"B.","family":"Blackham","sequence":"first","affiliation":[]},{"given":"G.","family":"Heiser","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","article-title":"The software model checker BLAST: Applications to software engineering","volume":"9","author":"beyer","year":"2007","journal-title":"Int J Softw Tools for Technology Transfer"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147002"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287655"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_23"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_18"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2011.15"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_34"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/WISES.2008.4623310"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_7"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2006.12"},{"key":"21","article-title":"TRACER: A symbolic execution tool for verification","author":"jaffar","year":"2012","journal-title":"10th CAV"},{"key":"20","first-page":"288","article-title":"Directed proof generation for machine code","author":"thakur","year":"2010","journal-title":"22nd CAV"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/2110356.2110358"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_27"},{"key":"24","first-page":"423","article-title":"Jakstab: A static analysis platform for binaries","author":"kinder","year":"2008","journal-title":"22nd CAV"},{"key":"25","first-page":"165","article-title":"The BINCOA framework for binary code analysis","author":"bardin","year":"2011","journal-title":"23rd CAV"},{"key":"26","first-page":"289","article-title":"ARMor: Fully verified software fault isolation","author":"zhao","year":"2011","journal-title":"11th EMSOFT"},{"key":"27","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/978-3-540-93900-9_19","article-title":"An abstract interpretation-based framework for control flow reconstruction from binaries","author":"kinder","year":"2009","journal-title":"10th Int Conf Verification Model Checking & Abstract Interpretation"},{"key":"28","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-642-18275-4_6","article-title":"Refinement-based CFG reconstruction from unstructured programs","author":"bardin","year":"2011","journal-title":"Proc Int Conf Verification Model Checking Abstract Interpretation"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(74)80049-8"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"2","article-title":"Operating systems technology for converged ECUs","author":"hergenhan","year":"2008","journal-title":"6th Emb Security in Cars Conf (escar)"},{"key":"10","first-page":"136","article-title":"A fast and precise static loop analysis based on abstract interpretation, program slicing and polytope models","author":"lokuciejewski","year":"2009","journal-title":"7th IEEE Symp Code Generation & Optimization"},{"year":"0","key":"1"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1145\/262004.262005"},{"key":"7","first-page":"137","article-title":"The Ma?lardalen WCET benchmarks-past, present and future","author":"gustafsson","year":"2010","journal-title":"7th WS Worst-Case Execution-Time Analysis"},{"key":"6","first-page":"243","article-title":"A trustworthy monadic formalization of the ARMv7 instruction set architecture","volume":"6172","author":"fox","year":"2010","journal-title":"1st ITP Ser LNCS"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/2168836.2168869"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"9","article-title":"Data-flow based detection of loop bounds","author":"cullmann","year":"2007","journal-title":"7th WS Worst-Case Execution-Time Analysis"},{"key":"8","first-page":"298","article-title":"Why model checking can improve WCET analysis","volume":"3114","author":"metzner","year":"2004","journal-title":"Computer Aided Verification Ser LNCS"}],"event":{"name":"2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS)","start":{"date-parts":[[2013,4,9]]},"location":"Philadelphia, PA","end":{"date-parts":[[2013,4,11]]}},"container-title":["2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6523367\/6531071\/06531083.pdf?arnumber=6531083","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T15:14:07Z","timestamp":1498058047000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6531083\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4]]},"references-count":33,"URL":"https:\/\/doi.org\/10.1109\/rtas.2013.6531083","relation":{},"subject":[],"published":{"date-parts":[[2013,4]]}}}