{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:24:20Z","timestamp":1768343060873,"version":"3.49.0"},"reference-count":28,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2023,4,2]],"date-time":"2023-04-02T00:00:00Z","timestamp":1680393600000},"content-version":"vor","delay-in-days":1462,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"},{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100001729","name":"Swedish Foundation for Strategic Research","doi-asserted-by":"publisher","award":["RIT 17-0036"],"award-info":[{"award-number":["RIT 17-0036"]}],"id":[{"id":"10.13039\/501100001729","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007294","name":"Swedish Civil Contingencies Agency","doi-asserted-by":"publisher","award":["2015-831"],"award-info":[{"award-number":["2015-831"]}],"id":[{"id":"10.13039\/501100007294","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1016\/j.scico.2019.01.001","type":"journal-article","created":{"date-parts":[[2019,1,17]],"date-time":"2019-01-17T12:58:01Z","timestamp":1547729881000},"page":"72-89","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":13,"special_numbering":"C","title":["TrABin: Trustworthy analyses of binaries"],"prefix":"10.1016","volume":"174","author":[{"given":"Andreas","family":"Lindner","sequence":"first","affiliation":[]},{"given":"Roberto","family":"Guanciale","sequence":"additional","affiliation":[]},{"given":"Roberto","family":"Metere","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2019.01.001_br0010","series-title":"International Conference on Information Systems Security","first-page":"1","article-title":"BitBlaze: a new approach to computer security via binary analysis","author":"Song","year":"2008"},{"key":"10.1016\/j.scico.2019.01.001_br0020","series-title":"Computer Aided Verification","first-page":"463","article-title":"BAP: a binary analysis platform","author":"Brumley","year":"2011"},{"key":"10.1016\/j.scico.2019.01.001_br0030","series-title":"Symposium on Security and Privacy","first-page":"138","article-title":"SOK: (state of) the art of war: offensive techniques in binary analysis","author":"Shoshitaishvili","year":"2016"},{"issue":"2","key":"10.1016\/j.scico.2019.01.001_br0040","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1016\/S1571-0661(04)81042-9","article-title":"Valgrind: a program supervision framework","volume":"89","author":"Nethercote","year":"2003","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2019.01.001_br0050","author":"Fox"},{"key":"10.1016\/j.scico.2019.01.001_br0060","series-title":"Interactive Theorem Proving","first-page":"338","article-title":"Directions in ISA Specification","author":"Fox","year":"2012"},{"key":"10.1016\/j.scico.2019.01.001_br0090","series-title":"Brazilian Symposium on Formal Methods","first-page":"197","article-title":"Sound transpilation from binary to machine-independent code","author":"Metere","year":"2017"},{"key":"10.1016\/j.scico.2019.01.001_br0100","series-title":"Operating Systems Principles","first-page":"207","article-title":"seL4: formal verification of an OS kernel","author":"Klein","year":"2009"},{"key":"10.1016\/j.scico.2019.01.001_br0110","series-title":"Verified Software: Theories, Tools, and Experiments","first-page":"209","article-title":"The Verisoft approach to systems verification","author":"Alkassar","year":"2008"},{"key":"10.1016\/j.scico.2019.01.001_br0120","series-title":"Workshop on Trustworthy Embedded Devices, Co-located with CCS","first-page":"3","article-title":"Machine code verification of a tiny ARM hypervisor","author":"Dam","year":"2013"},{"issue":"7","key":"10.1016\/j.scico.2019.01.001_br0130","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","article-title":"Formal verification of a realistic compiler","volume":"52","author":"Leroy","year":"2009","journal-title":"Commun. ACM"},{"key":"10.1016\/j.scico.2019.01.001_br0140","series-title":"Symposium on Computer Arithmetic","first-page":"107","article-title":"A formally-verified C compiler supporting floating-point arithmetic","author":"Boldo","year":"2013"},{"key":"10.1016\/j.scico.2019.01.001_br0150","first-page":"179","article-title":"CakeML: a verified implementation of ML","volume":"vol. 49","author":"Kumar","year":"2014"},{"key":"10.1016\/j.scico.2019.01.001_br0160","series-title":"European Symposium on Programming","first-page":"205","article-title":"Structure of a proof-producing compiler for a subset of higher order logic","author":"Li","year":"2007"},{"key":"10.1016\/j.scico.2019.01.001_br0170","series-title":"USENIX Security Symposium","first-page":"207","article-title":"Verified correctness and security of OpenSSL HMAC","author":"Beringer","year":"2015"},{"key":"10.1016\/j.scico.2019.01.001_br0180","series-title":"Design and Verification of Microprocessor Systems for High-assurance Applications","first-page":"221","article-title":"Specification and verification of ARM hardware and software","author":"Fox","year":"2010"},{"key":"10.1016\/j.scico.2019.01.001_br0190","series-title":"Formal Methods in Computer-Aided Design","first-page":"1","article-title":"Machine-code verification for multiple architectures \u2013 an application of decompilation into logic","author":"Myreen","year":"2008"},{"key":"10.1016\/j.scico.2019.01.001_br0200","series-title":"SIGPLAN Conference on Programming Language Design and Implementation","first-page":"471","article-title":"Translation validation for a verified OS kernel","author":"Sewell","year":"2013"},{"key":"10.1016\/j.scico.2019.01.001_br0210","series-title":"Certified Programs and Proofs \u2013 Third International Conference","first-page":"66","article-title":"Proof pearl: a verified bignum implementation in x86-64 machine code","author":"Myreen","year":"2013"},{"key":"10.1016\/j.scico.2019.01.001_br0220","series-title":"SIGSAC Conference on Computer and Communications Security","first-page":"1080","article-title":"Automating information flow analysis of low level code","author":"Balliu","year":"2014"},{"issue":"1","key":"10.1016\/j.scico.2019.01.001_br0230","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/2756550","article-title":"Cacheaudit: a tool for the static analysis of cache side channels","volume":"18","author":"Doychev","year":"2015","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"2","key":"10.1016\/j.scico.2019.01.001_br0240","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1145\/2954680.2872380","article-title":"Lifting assembly to intermediate representation: a novel approach leveraging compilers","volume":"50","author":"Hasabnis","year":"2016","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"10.1016\/j.scico.2019.01.001_br0250","series-title":"Symposium on Applied Computing","first-page":"2517","article-title":"A machine-checked soundness proof for an efficient verification condition generator","author":"Vogels","year":"2010"},{"issue":"6","key":"10.1016\/j.scico.2019.01.001_br0260","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","article-title":"Efficient weakest preconditions","volume":"93","author":"Leino","year":"2005","journal-title":"Inf. Process. Lett."},{"key":"10.1016\/j.scico.2019.01.001_br0270","series-title":"Conference on Computer and Communications Security","first-page":"552","article-title":"The geometry of innocent flesh on the bone: return-into-libc without function calls (on the x86)","author":"Shacham","year":"2007"},{"key":"10.1016\/j.scico.2019.01.001_br0280","series-title":"Symposium on Information, Computer and Communications Security","first-page":"30","article-title":"Jump-oriented programming: a new class of code-reuse attack","author":"Bletsch","year":"2011"},{"key":"10.1016\/j.scico.2019.01.001_br0290","series-title":"Certified Programs and Proofs: First International Conference","first-page":"183","article-title":"Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle\/HOL","author":"B\u00f6hme","year":"2011"},{"key":"10.1016\/j.scico.2019.01.001_br0300","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"337","article-title":"Z3: an efficient SMT solver","author":"de Moura","year":"2008"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642318301667?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642318301667?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T22:47:02Z","timestamp":1759099622000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642318301667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4]]},"references-count":28,"alternative-id":["S0167642318301667"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2019.01.001","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2019,4]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"TrABin: Trustworthy analyses of binaries","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2019.01.001","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2019 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}