{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,10]],"date-time":"2026-09-10T17:06:00Z","timestamp":1789059960952,"version":"build-2803163510"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Rajiv and Ritu Batra","award":["Gift"],"award-info":[{"award-number":["Gift"]}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-14-2-0270"],"award-info":[{"award-number":["FA8750-14-2-0270"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1423237"],"award-info":[{"award-number":["CCF-1423237"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"UW-Madison Office of the Vice Chancellor for Research and Graduate Education"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2017,10,12]]},"abstract":"<jats:p>Binary rewriters are tools that are used to modify the functionality of binaries lacking source code. Binary rewriters can be used to rewrite binaries for a variety of purposes including optimization, hardening, and extraction of executable components. To rewrite a binary based on semantic criteria, an essential primitive to have is a machine-code synthesizer---a tool that synthesizes an instruction sequence from a specification of the desired behavior, often given as a formula in quantifier-free bit-vector logic (QFBV). However, state-of-the-art machine-code synthesizers such as McSynth++ employ naive search strategies for synthesis: McSynth++ merely enumerates candidates of increasing length without performing any form of prioritization. This inefficient search strategy is compounded by the huge number of unique instruction schemas in instruction sets (e.g., around 43,000 in Intel's IA-32) and the exponential cost inherent in enumeration. The effect is slow synthesis: even for relatively small specifications, McSynth++ might take several minutes or a few hours to find an implementation.<\/jats:p>\n                  <jats:p>In this paper, we describe how we use machine learning to make the search in McSynth++ smarter and potentially faster. We converted the linear search in McSynth++ into a best-first search over the space of instruction sequences. The cost heuristic for the best-first search comes from two models---used together---built from a corpus of \u2329QFBV-formula, instruction-sequence\u232a pairs: (i) a language model that favors useful instruction sequences, and (ii) a regression model that correlates features of instruction sequences with features of QFBV formulas, and favors instruction sequences that are more likely to implement the input formula. Our experiments for IA-32 showed that our model-assisted synthesizer enables synthesis of code for 6 out of 50 formulas on which McSynth++ times out, speeding up the synthesis time by at least 549X, and for the remaining formulas, speeds up synthesis by 4.55X.<\/jats:p>","DOI":"10.1145\/3133885","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T11:15:45Z","timestamp":1507893345000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Model-assisted machine-code synthesis"],"prefix":"10.1145","volume":"1","author":[{"given":"Venkatesh","family":"Srinivasan","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ara","family":"Vartanian","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA \/ GrammaTech, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"M. Abadi M. Budiu U. Erlingsson and J. Ligatti. 2005. Control-flow Integrity. In CCS. 10.1145\/1102120.1102165","DOI":"10.1145\/1102120.1102165"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749612"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"S. Bansal and A. Aiken. 2006. Automatic Generation of Peephole Superoptimizers. In ASPLOS. 10.1145\/1168857.1168906","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_2_1_4_1","unstructured":"S. Bansal and A. Aiken. 2008. Binary Translation Using Peephole Superoptimizers. In OSDI."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_37"},{"key":"e_1_2_1_6_1","volume-title":"Yices: An SMT Solver.","author":"Dutertre B.","year":"2006","unstructured":"B. Dutertre and L. de Moura. 2006. Yices: An SMT Solver. (2006). http:\/\/yices.csl.sri.com\/."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"K. ElWazeer K. Anand A. Kotha M. Smithson and R. Barua. 2013. Scalable Variable and Data Type Detection in a Binary Rewriter. In PLDI. 10.1145\/2491956.2462165","DOI":"10.1145\/2491956.2462165"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"T. Gvero and V. Kuncak. 2015. Synthesizing Java expressions from free-form queries. In OOPSLA. 10.1145\/2814270.2814295","DOI":"10.1145\/2814270.2814295"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1186736.1186737"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"B. Hsu and J. Glass. 2008. Iterative Language Model Estimation: Efficient Data Structure and Algorithms. In Interspeech.","DOI":"10.21437\/Interspeech.2008-255"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512566"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220921.3221245"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_2_1_14_1","volume-title":"Superoptimizer: A Look at the Smallest Program. In ASPLOS.","author":"Massalin H.","year":"1987","unstructured":"H. Massalin. 1987. Superoptimizer: A Look at the Smallest Program. In ASPLOS."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1953048.2078195"},{"key":"e_1_2_1_16_1","unstructured":"P. Phothilimthana A. Thakur R. Bodik and D. Ghurjati. 2016a. GreenThumb: Superoptimizer Construction Framework. UCB\/EECS-2016-8. University of California\u2013Berkeley Tech Report. http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2016\/ EECS- 2016- 8.pdf"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"P. Phothilimthana A. Thakur R. Bodik and D. Ghurjati. 2016b. Scaling up Superoptimization. In ASPLOS. 10.1145\/2872362.2872387","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"V. Raychev M. Vechev and A. Krause. 2015. Predicting Program Properties from\u201cBig Code\". In POPL.","DOI":"10.1145\/2676726.2677009"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"V. Raychev M. Vechev and E. Yahav. 2014. Code Completion with Statistical Language Models. In PLDI. 10.1145\/2666356.2594321","DOI":"10.1145\/2666356.2594321"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1387830.1387837"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"E. Schkufza R. Sharma and A. Aiken. 2013. Stochastic Superoptimization. In ASPLOS. 10.1145\/2451116.2451150","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_2_1_22_1","unstructured":"A. Slowinska T. Stancescu and H. Bos. 2012. Body Armor for Binaries: Preventing Buffer Overflows Without Recompilation. In ATC."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89862-7_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"V. Srinivasan and T. Reps. 2015a. Partial Evaluation of Machine Code. In OOPSLA. 10.1145\/2814270.2814321","DOI":"10.1145\/2814270.2814321"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"V. Srinivasan and T. Reps. 2015b. Synthesis of Machine Code from Semantics. In PLDI. 10.1145\/2737924.2737960","DOI":"10.1145\/2737924.2737960"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"V. Srinivasan and T. Reps. 2016. An Improved Algorithm for Slicing Machince Code. In OOPSLA.","DOI":"10.1145\/2983990.2984003"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"V. Srinivasan T. Sharma and T. Reps. 2016. Speeding-up Machine-Code Synthesis. In OOPSLA. 10.1145\/2983990.2984006","DOI":"10.1145\/2983990.2984006"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"B. Yadegari B. Johannesmeyer B. Whitely and S. Debray. 2015. A Generic Approach to Automatic Deobfuscation of Executable Code. In S&amp;P. 10.1109\/SP.2015.47","DOI":"10.1109\/SP.2015.47"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133885","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133885","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133885","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,10]],"date-time":"2026-09-10T16:07:16Z","timestamp":1789056436000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133885"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":28,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3133885"],"URL":"https:\/\/doi.org\/10.1145\/3133885","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}