{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:44:49Z","timestamp":1748583889118,"version":"3.37.3"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,9,9]],"date-time":"2017-09-09T00:00:00Z","timestamp":1504915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,9,9]],"date-time":"2017-09-09T00:00:00Z","timestamp":1504915200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["CCF-1624124"],"award-info":[{"award-number":["CCF-1624124"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000083","name":"irectorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["CNS-1624126"],"award-info":[{"award-number":["CNS-1624126"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,3]]},"DOI":"10.1007\/s10817-017-9429-1","type":"journal-article","created":{"date-parts":[[2017,9,11]],"date-time":"2017-09-11T19:52:27Z","timestamp":1505159547000},"page":"257-277","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Bidirectional Grammars for Machine-Code Decoding and Encoding"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6109-6091","authenticated-orcid":false,"given":"Gang","family":"Tan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,9]]},"reference":[{"key":"9429_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Budiu, M., Erlingsson, \u00da., Ligatti, J.: Control-flow integrity. In: 12th ACM Conference on Computer and Communications Security (CCS), pp. 340\u2013353 (2005)","DOI":"10.1145\/1102120.1102165"},{"key":"9429_CR2","doi-asserted-by":"crossref","unstructured":"Alimarine, A., Smetsers, S., van Weelden, A., van Eekelen, M.C.J.D., Plasmeijer, R.: There and back again: arrows for invertible programming. In: Proceedings of the ACM SIGPLAN Workshop on Haskell, pp. 86\u201397 (2005)","DOI":"10.1145\/1088348.1088357"},{"key":"9429_CR3","unstructured":"Bergeron, J., Debbabi, M., Desharnais, J., Erhioui, M., Lavoie, Y., Tawbi, N.: Static detection of malicious code in executable programs. Int. J. Requir. Eng. (2001)"},{"key":"9429_CR4","doi-asserted-by":"crossref","unstructured":"Bohannon, A., Foster, J.N., Pierce, B.C., Pilkiewicz, A., Schmitt, A.: Boomerang: resourceful lenses for string data. In: 35th ACM Symposium on Principles of Programming Languages (POPL), pp. 407\u2013419 (2008)","DOI":"10.1145\/1328897.1328487"},{"key":"9429_CR5","doi-asserted-by":"crossref","unstructured":"Brabrand, C., M\u00f8ller, A., Schwartzbach, M.I.: Dual syntax for XML languages. In: 10th International Symposium on Database Programming Languages (DBPL), pp. 27\u201341 (2005)","DOI":"10.1007\/11601524_2"},{"key":"9429_CR6","doi-asserted-by":"crossref","unstructured":"Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: a binary analysis platform. In: Computer Aided Verification (CAV), pp. 463\u2013469 (2011)","DOI":"10.1007\/978-3-642-22110-1_37"},{"key":"9429_CR7","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11, 481\u2013494 (1964)","journal-title":"J. ACM"},{"key":"9429_CR8","unstructured":"Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. In: 12th Usenix Security Symposium, pp. 169\u2013186 (2003)"},{"key":"9429_CR9","unstructured":"The Coq proof assistant. \n                    https:\/\/coq.inria.fr\/"},{"key":"9429_CR10","doi-asserted-by":"crossref","unstructured":"Ford, B.: Parsing expression grammars: A recognition-based syntactic foundation. In: 31st ACM Symposium on Principles of Programming Languages (POPL), pp. 111\u2013122 (2004)","DOI":"10.1145\/964001.964011"},{"key":"9429_CR11","doi-asserted-by":"crossref","unstructured":"Fox, A.C.J.: Improved tool support for machine-code decompilation in HOL4. In: 6th International Conference on Interactive Theorem Proving (ITP), pp. 187\u2013202 (2015)","DOI":"10.1007\/978-3-319-22102-1_12"},{"key":"9429_CR12","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network and Distributed System Security Symposium (NDSS) (2008)"},{"key":"9429_CR13","doi-asserted-by":"crossref","unstructured":"Jansson, P., Jeuring, J.: Polytypic compact printing and parsing. In: 8th European Symposium on Programming (ESOP), pp. 273\u2013287 (1999)","DOI":"10.1007\/3-540-49099-X_18"},{"key":"9429_CR14","doi-asserted-by":"crossref","unstructured":"Jourdan, J.H., Pottier, F., Leroy, X.: Validating LR(1) parsers. In: European Symposium on Programming (ESOP), pp. 397\u2013416 (2012)","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"9429_CR15","doi-asserted-by":"crossref","unstructured":"Kawanaka, S., Hosoya, H.: biXid: a bidirectional transformation language for XML. In: ACM International Conference on Functional programming (ICFP), pp. 201\u2013214 (2006)","DOI":"10.1145\/1160074.1159830"},{"issue":"6","key":"9429_CR16","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1017\/S0956796804005209","volume":"14","author":"A Kennedy","year":"2004","unstructured":"Kennedy, A.: Pickler combinators. J. Funct. Program. 14(6), 727\u2013739 (2004)","journal-title":"J. Funct. Program."},{"key":"9429_CR17","unstructured":"Kotha, A., Anand, K., Smithson, M., Yellareddy, G., Barua, R.: Automatic parallelization in a binary rewriter. In: Proceedings of the 43rd Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO), 2010, pp. 547\u2013557 (2010)"},{"key":"9429_CR18","unstructured":"Kroll, J., Dean, D.: BakerSFIeld: Bringing software fault isolation to x64. \n                    www.jkroll.com\/papers\/bakersfield_sfi.pdf"},{"key":"9429_CR19","unstructured":"McCamant, S., Morrisett, G.: Evaluating SFI for a CISC architecture. In: 15th Usenix Security Symposium (2006)"},{"key":"9429_CR20","doi-asserted-by":"crossref","unstructured":"Might, M., Darais, D., Spiewak, D.: Parsing with derivatives: a functional pearl. In: ACM International Conference on Functional programming (ICFP), pp. 189\u2013195 (2011)","DOI":"10.1145\/2034574.2034801"},{"key":"9429_CR21","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.B., Gan, E.: Rocksalt: better, faster, stronger SFI for the x86. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 395\u2013404 (2012)","DOI":"10.1145\/2345156.2254111"},{"key":"9429_CR22","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1017\/S0956796808007090","volume":"19","author":"S Owens","year":"2009","unstructured":"Owens, S., Reppy, J., Turon, A.: Regular-expression derivatives re-examined. J. Funct. Program. 19, 173\u2013190 (2009)","journal-title":"J. Funct. Program."},{"issue":"3","key":"9429_CR23","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1145\/256167.256225","volume":"19","author":"N Ramsey","year":"1997","unstructured":"Ramsey, N., Fern\u00e1ndez, M.F.: Specifying representations of machine instructions. ACM Trans. Program. Lang. Syst. 19(3), 492\u2013524 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9429_CR24","doi-asserted-by":"crossref","unstructured":"Rendel, T., Ostermann, K.: Invertible syntax descriptions: unifying parsing and pretty printing. In: Third ACM Haskell Symposium on Haskell, pp. 1\u201312 (2010)","DOI":"10.1145\/2088456.1863525"},{"key":"9429_CR25","doi-asserted-by":"crossref","unstructured":"Reps, T., Lim, J., Thakur, A., Balakrishnan, G., Lal, A.: There\u2019s plenty of room at the bottom: analyzing and verifying machine code. In: Computer Aided Verification (CAV), pp. 41\u201356 (2010)","DOI":"10.1007\/978-3-642-14295-6_6"},{"key":"9429_CR26","doi-asserted-by":"crossref","unstructured":"Sepp, A., Kranz, J., Simon, A.: GDSL: a generic decoder specification language for interpreting machine language. In: Tools for Automatic Program Analysis, pp. 53\u201364 (2012)","DOI":"10.1016\/j.entcs.2012.11.006"},{"key":"9429_CR27","doi-asserted-by":"crossref","unstructured":"Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M.G., Liang, Z., Newsome, J., Poosankam, P., Saxena, P.: BitBlaze: A new approach to computer security via binary analysis. In: Proceedings of the 4th International Conference on Information Systems Security (2008)","DOI":"10.1007\/978-3-540-89862-7_1"},{"key":"9429_CR28","doi-asserted-by":"crossref","unstructured":"Tan, G., Morrisett, G.: Bidirectional grammars for machine-code decoding and encoding. In: 8th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), pp. 73\u201389 (2016)","DOI":"10.1007\/978-3-319-48869-1_6"},{"key":"9429_CR29","doi-asserted-by":"crossref","unstructured":"Wahbe, R., Lucco, S., Anderson, T., Graham, S.: Efficient software-based fault isolation. In: ACM SIGOPS Symposium on Operating Systems Principles (SOSP), pp. 203\u2013216. ACM Press, New York (1993)","DOI":"10.1145\/173668.168635"},{"key":"9429_CR30","doi-asserted-by":"crossref","unstructured":"Wartell, R., Mohan, V., Hamlen, K.W., Lin, Z.: Securing untrusted code via compiler-agnostic binary rewriting. In: Proceedings of the 28th Annual Computer Security Applications Conference, pp. 299\u2013308 (2012)","DOI":"10.1145\/2420950.2420995"},{"key":"9429_CR31","doi-asserted-by":"crossref","unstructured":"Xu, Z., Miller, B., Reps, T.: Safety checking of machine code. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 70\u201382 (2000)","DOI":"10.1145\/358438.349313"},{"key":"9429_CR32","doi-asserted-by":"crossref","unstructured":"Yee, B., Sehr, D., Dardyk, G., Chen, B., Muth, R., Ormandy, T., Okasaka, S., Narula, N., Fullagar, N.: Native client: A sandbox for portable, untrusted x86 native code. In: IEEE Symposium on Security and Privacy (S&P) (2009)","DOI":"10.1109\/SP.2009.25"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9429-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9429-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9429-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T23:02:19Z","timestamp":1589410939000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9429-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,9]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,3]]}},"alternative-id":["9429"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9429-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,9,9]]},"assertion":[{"value":"29 August 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 August 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 September 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}