{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:35:45Z","timestamp":1770276945686,"version":"3.49.0"},"reference-count":33,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987600","type":"proceedings-article","created":{"date-parts":[[2014,12,30]],"date-time":"2014-12-30T20:00:39Z","timestamp":1419969639000},"page":"91-98","source":"Crossref","is-referenced-by-count":24,"title":["Simulation and formal verification of x86 machine-code programs that make system calls"],"prefix":"10.1109","author":[{"given":"Shilpi","family":"Goel","sequence":"first","affiliation":[]},{"given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[]},{"given":"Soumava","family":"Ghosh","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","year":"0","journal-title":"Linux"},{"key":"17","article-title":"Formal verification of machine-code programs","author":"myreen","year":"2008","journal-title":"British Computer Society"},{"key":"18","first-page":"78","article-title":"Decompilation into logic-improved","volume":"2012","author":"myreen","year":"2012","journal-title":"Formal Methods in Computer-Aided Design (FMCAD"},{"key":"33","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/2450136.2450139","article-title":"Tsl: A system for generating abstract interpreters and its application to machine-code analysis","volume":"35","author":"lim","year":"2013","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9098-1"},{"key":"16","author":"moore","year":"0","journal-title":"Code Walker Tool"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_12"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243131"},{"key":"11","author":"kernighan","year":"1988","journal-title":"The C Programming Language"},{"key":"12","author":"newlib","year":"0","journal-title":"Newlib C Library"},{"key":"21","author":"moore","year":"1996","journal-title":"Piton A Mechanically Verified Assembly-level Language"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243132"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_23"},{"key":"23","author":"degenbaev","year":"2012","journal-title":"Formal Specification of the x86 Instruction Set Architecture"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008624904634"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04468-7_16"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"28","year":"0","journal-title":"The Coq Proof Assistant"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9118-9"},{"key":"3","article-title":"A formal model of a large memory that supports efficient execution","author":"hunt","year":"2012","journal-title":"Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD"},{"key":"2","article-title":"Mechanized operational semantics","author":"moore","year":"2008","journal-title":"Lectures in the Marktoberdorf Summer School"},{"key":"10","author":"matz","year":"0","journal-title":"System v Application Binary Interface AMD64 Architecture Processor Supplement"},{"key":"1","author":"kaufmann","year":"2012","journal-title":"Towards A Formal Model of the x86 ISA"},{"key":"30","first-page":"469","article-title":"Towards machine-verified proofs for i\/o","author":"dowse","year":"2004","journal-title":"Technical Report 0408 in the Proceedings of Implementation and Application of Functional Languages 16th International Workshop IFL'04"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2007.07.002"},{"key":"6","year":"0","journal-title":"Intel Intel 64 and IA-32 Architectures Software Developer's Manuals"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.08.004"},{"key":"5","year":"0","journal-title":"Intel Pin-A Dynamic Binary Instrumentation Tool"},{"key":"31","author":"de mol","year":"2007","journal-title":"The Mathematical Foundation of the Proof Assistant Sparkle"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.114.5"},{"key":"9","author":"kerrisk","year":"2010","journal-title":"The LINUX Programming Interface"},{"key":"8","year":"0","journal-title":"CCL CCL Manual Foreign Function Interface"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","location":"Lausanne, Switzerland","start":{"date-parts":[[2014,10,21]]},"end":{"date-parts":[[2014,10,24]]}},"container-title":["2014 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6975680\/6987576\/06987600.pdf?arnumber=6987600","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T23:19:19Z","timestamp":1566170359000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987600\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":33,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987600","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}