{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:11Z","timestamp":1772164091980,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":69,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,4,4]],"date-time":"2017-04-04T00:00:00Z","timestamp":1491264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1239567, 1162187, 1563935"],"award-info":[{"award-number":["1239567, 1162187, 1563935"]}],"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":[[2017,4,4]]},"DOI":"10.1145\/3037697.3037733","type":"proceedings-article","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T08:47:40Z","timestamp":1491382060000},"page":"177-191","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["An Architecture Supporting Formal and Compositional Binary Analysis"],"prefix":"10.1145","author":[{"given":"Joseph","family":"McMahan","sequence":"first","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, CA, USA"}]},{"given":"Michael","family":"Christensen","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, CA, USA"}]},{"given":"Lawton","family":"Nichols","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, CA, USA"}]},{"given":"Jared","family":"Roesch","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, Seattle, WA, USA"}]},{"given":"Sung-Yee","family":"Guo","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, CA, USA"}]},{"given":"Ben","family":"Hardekopf","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, CA, USA"}]},{"given":"Timothy","family":"Sherwood","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,4,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"The Coq proof assistant: https:\/\/coq.inria.fr.  The Coq proof assistant: https:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_2_1","unstructured":"How many people have ICDs? http:\/\/asktheicd.com\/tile\/106\/english-implantable-cardioverter-defibrillator-icd\/how-many-people-have-icds\/.  How many people have ICDs? http:\/\/asktheicd.com\/tile\/106\/english-implantable-cardioverter-defibrillator-icd\/how-many-people-have-icds\/."},{"key":"e_1_3_2_1_3_1","unstructured":"Living with your implantable cardioverter defibrillator (ICD). http:\/\/www.heart.org\/HEARTORG\/Conditions\/Arrhythmia\/PreventionTreatmentofArrhythmia\/Living-With-Your-Implantable-Cardioverter-Defibrillator-ICD_UCM_448462_Article.jsp.  Living with your implantable cardioverter defibrillator (ICD). http:\/\/www.heart.org\/HEARTORG\/Conditions\/Arrhythmia\/PreventionTreatmentofArrhythmia\/Living-With-Your-Implantable-Cardioverter-Defibrillator-ICD_UCM_448462_Article.jsp."},{"key":"e_1_3_2_1_4_1","unstructured":"Open source ECG analysis software. http:\/\/www.eplimited.com\/confirmation.htm.  Open source ECG analysis software. http:\/\/www.eplimited.com\/confirmation.htm."},{"key":"e_1_3_2_1_5_1","unstructured":"Journal of Automated Reasoning 30(3--4) 2003.  Journal of Automated Reasoning 30(3--4) 2003."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_181"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.77"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/800087.802798"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1161\/01.CIR.101.11.1297"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/366663.366704"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICESS.2009.82"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"M. M. Cruz-Cunha J. Varaj\u00e3o H. Krcmar R. Martinho R. A. \u00c1lvarez A. J. M. Pen\u00edn and X. A. V. Sobrino. Centeris 2013 - conference on enterprise information systems \/ projman 2013 - international conference on project management\/ hcist 2013 - international conference on health and social care information systems and technologies a comparison of three qrs detection algorithms over a public database. Procedia Technology 9:1159 -- 1165 2013.  M. M. Cruz-Cunha J. Varaj\u00e3o H. Krcmar R. Martinho R. A. \u00c1lvarez A. J. M. Pen\u00edn and X. A. V. Sobrino. Centeris 2013 - conference on enterprise information systems \/ projman 2013 - international conference on project management\/ hcist 2013 - international conference on health and social care information systems and technologies a comparison of three qrs detection algorithms over a public database. Procedia Technology 9:1159 -- 1165 2013.","DOI":"10.1016\/j.protcy.2013.12.129"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/HOL.1991.596292"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_3_2_1_21_1","volume-title":"HotSec","author":"Denning T.","year":"2008","unstructured":"T. Denning , K. Fu , and T. Kohno . Absence makes the heart grow fonder: New directions for implantable medical device security . In HotSec , 2008 . T. Denning, K. Fu, and T. Kohno. Absence makes the heart grow fonder: New directions for implantable medical device security. In HotSec, 2008."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1624775.1624860"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018438"},{"key":"e_1_3_2_1_26_1","first-page":"692","volume-title":"Formal Specification of a Cardiac Pacing System","author":"Gomes A. O.","year":"2009","unstructured":"A. O. Gomes and M. V. M. Oliveira . Formal Specification of a Cardiac Pacing System , pages 692 -- 707 . Springer Berlin Heidelberg , Berlin, Heidelberg , 2009 . A. O. Gomes and M. V. M. Oliveira. Formal Specification of a Cardiac Pacing System, pages 692--707. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009."},{"key":"e_1_3_2_1_27_1","volume-title":"Design issues. Technical report","author":"Graham B.","year":"1989","unstructured":"B. Graham . Secd : Design issues. Technical report , University of Calgary , 1989 . B. Graham. Secd: Design issues. Technical report, University of Calgary, 1989."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.31"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2011.5764696"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268976"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/1995158"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1238844.1238856"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243132"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2161241"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.19"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1816038.1816010"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_40_1","unstructured":"P. M. Kogge. \"The Architecture of Symbolic Computers\". McGraw-Hill Inc. New York New York 1991.  P. M. Kogge. \"The Architecture of Symbolic Computers\". McGraw-Hill Inc. New York New York 1991."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1929004.1929005"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMSNETS.2016.7440015"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1357010.1352625"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_2"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243133"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462166.1462167"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0413-8_8"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/TBME.1985.325532"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693167"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_23"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1155\/2015\/939028"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/0002-8703(94)90101-5"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2002.1021818"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45620-1_5"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364524"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1056\/NEJM199711273372202"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1161\/01.CIR.0000145610.64014.E4"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507657"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36575-3_25"}],"event":{"name":"ASPLOS '17: Architectural Support for Programming Languages and Operating Systems","location":"Xi'an China","acronym":"ASPLOS '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3037697.3037733","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3037697.3037733","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3037697.3037733","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:03:10Z","timestamp":1750201390000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3037697.3037733"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,4]]},"references-count":69,"alternative-id":["10.1145\/3037697.3037733","10.1145\/3037697"],"URL":"https:\/\/doi.org\/10.1145\/3037697.3037733","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093337.3037733","asserted-by":"object"},{"id-type":"doi","id":"10.1145\/3093336.3037733","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,4,4]]},"assertion":[{"value":"2017-04-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}