{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T11:14:55Z","timestamp":1769771695574,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,25]],"date-time":"2017-10-25T00:00:00Z","timestamp":1508889600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,25]]},"DOI":"10.1145\/3133850.3133856","type":"proceedings-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T15:16:02Z","timestamp":1507907762000},"page":"78-88","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Unbounded superoptimization"],"prefix":"10.1145","author":[{"given":"Abhinav","family":"Jangda","sequence":"first","affiliation":[{"name":"IIT Varanasi, India"}]},{"given":"Greta","family":"Yorsh","sequence":"additional","affiliation":[{"name":"Queen Mary University of London, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,10,25]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"ISA specification for ARMv8-A. (2017). https:\/\/developer. arm.com\/products\/architecture\/a-profile\/exploration-tools , released","author":"ARM.","year":"2017","unstructured":"ARM. 2017. ISA specification for ARMv8-A. (2017). https:\/\/developer. arm.com\/products\/architecture\/a-profile\/exploration-tools , released in April 2017 . ARM. 2017. ISA specification for ARMv8-A. (2017). https:\/\/developer. arm.com\/products\/architecture\/a-profile\/exploration-tools , released in April 2017."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_29"},{"key":"e_1_3_2_1_5_1","volume-title":"Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). 15\u201327","author":"Bj\u00f8rner Nikolaj","year":"2015","unstructured":"Nikolaj Bj\u00f8rner and Mikol\u00e1s Janota . 2015 . Playing with Quantified Satisfaction (short paper) . In Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). 15\u201327 . Nikolaj Bj\u00f8rner and Mikol\u00e1s Janota. 2015. Playing with Quantified Satisfaction (short paper). In Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). 15\u201327."},{"key":"e_1_3_2_1_6_1","volume-title":"Maximum Satisfiability Using Cores and Correction Sets. In Int. Joint Conf. on Artificial Intelligence (IJCAI). 246\u2013252","author":"Bj\u00f8rner Nikolaj","year":"2015","unstructured":"Nikolaj Bj\u00f8rner and Nina Narodytska . 2015 . Maximum Satisfiability Using Cores and Correction Sets. In Int. Joint Conf. on Artificial Intelligence (IJCAI). 246\u2013252 . Nikolaj Bj\u00f8rner and Nina Narodytska. 2015. Maximum Satisfiability Using Cores and Correction Sets. In Int. Joint Conf. on Artificial Intelligence (IJCAI). 246\u2013252."},{"key":"e_1_3_2_1_7_1","volume-title":"Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 194\u2013199","author":"Bj\u00f8rner Nikolaj","year":"2015","unstructured":"Nikolaj Bj\u00f8rner , Anh-Dung Phan , and Lars Fleckenstein . 2015 . \u03bd Z -An Optimizing SMT Solver . In Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 194\u2013199 . Nikolaj Bj\u00f8rner, Anh-Dung Phan, and Lars Fleckenstein. 2015. \u03bd Z -An Optimizing SMT Solver. In Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 194\u2013199."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11799573_21"},{"key":"e_1_3_2_1_11_1","volume-title":"Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"Bjorner N.","year":"2008","unstructured":"Bjorner N. de Maura L. 2008 . Z3: An efficient SMT solver . In Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Bjorner N. de Maura L. 2008. Z3: An efficient SMT solver. In Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Leonardo Mendon\u00e7a de Moura and Grant Olney Passmore. 2013. The Strategy Challenge in SMT Solving. In Automated Reasoning and Mathematics - Essays in Memory of William W. McCune. 15\u201344.  Leonardo Mendon\u00e7a de Moura and Grant Olney Passmore. 2013. The Strategy Challenge in SMT Solving. In Automated Reasoning and Mathematics - Essays in Memory of William W. McCune. 15\u201344.","DOI":"10.1007\/978-3-642-36675-8_2"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_23"},{"key":"e_1_3_2_1_16_1","volume-title":"Proc. of Association for the Advancement of Artificial Intelligence (AAAI). 1136\u20131143","author":"Fr\u00f6hlich Andreas","year":"2015","unstructured":"Andreas Fr\u00f6hlich , Armin Biere , Christoph M Wintersteiger , and Youssef Hamadi . 2015 . Stochastic Local Search for Satisfiability Modulo Theories . In Proc. of Association for the Advancement of Artificial Intelligence (AAAI). 1136\u20131143 . Andreas Fr\u00f6hlich, Armin Biere, Christoph M Wintersteiger, and Youssef Hamadi. 2015. Stochastic Local Search for Satisfiability Modulo Theories. In Proc. of Association for the Advancement of Artificial Intelligence (AAAI). 1136\u20131143."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-010-0161-2"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869463"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512566"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491452"},{"key":"e_1_3_2_1_24_1","volume-title":"SIGPLAN Conf. on Prog. Lang. Design and Impl. (PLDI). ACM.","author":"Ed Monica S.","year":"2000","unstructured":"Monica S. Lam ( Ed .). 2000 . SIGPLAN Conf. on Prog. Lang. Design and Impl. (PLDI). ACM. Monica S. Lam (Ed.). 2000. SIGPLAN Conf. on Prog. Lang. Design and Impl. (PLDI). ACM."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0158-6"},{"key":"e_1_3_2_1_27_1","article-title":"TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code","volume":"35","author":"Lim Junghee","year":"2013","unstructured":"Junghee Lim and Thomas W. Reps . 2013 . TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis. Trans. on Prog. Lang. and Syst. (TOPLAS) 35 , 1, Article 4 (2013). Junghee Lim and Thomas W. Reps. 2013. TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis. Trans. on Prog. Lang. and Syst. (TOPLAS) 35, 1, Article 4 (2013).","journal-title":"Analysis. Trans. on Prog. Lang. and Syst. (TOPLAS)"},{"key":"e_1_3_2_1_28_1","volume-title":"Provably Correct Peephole Optimizations with Alive. In SIGPLAN Conf. on Prog. Lang. Design and Impl. (PLDI). http: \/\/web.ist.utl.pt\/nuno.lopes\/pubs.php?id=alive-pldi15 .","author":"Lopes Nuno P.","year":"2015","unstructured":"Nuno P. Lopes , David Menendez , Santosh Nagarakatte , and John Regehr . 2015 . Provably Correct Peephole Optimizations with Alive. In SIGPLAN Conf. on Prog. Lang. Design and Impl. (PLDI). http: \/\/web.ist.utl.pt\/nuno.lopes\/pubs.php?id=alive-pldi15 . Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. 2015. Provably Correct Peephole Optimizations with Alive. In SIGPLAN Conf. on Prog. Lang. Design and Impl. (PLDI). http: \/\/web.ist.utl.pt\/nuno.lopes\/pubs.php?id=alive-pldi15 ."},{"key":"e_1_3_2_1_29_1","volume-title":"Int. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS).","author":"Massalin Henry","year":"1987","unstructured":"Henry Massalin . 1987 . Superoptimizer: A look at the smallest program . In Int. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS). Henry Massalin. 1987. Superoptimizer: A look at the smallest program. In Int. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS)."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_21"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Alastair Reid. 2016. Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture. In Formal Methods in Computer-Aided Design (FMCAD).  Alastair Reid. 2016. Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture. In Formal Methods in Computer-Aided Design (FMCAD).","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594302"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509509"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814278"},{"key":"e_1_3_2_1_39_1","volume-title":"CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. 68\u201394","author":"Si Xujie","year":"2017","unstructured":"Xujie Si , Xin Zhang , Radu Grigore , and Mayur Naik . 2017 . Maximum Satisfiability in Software Analysis: Applications and Techniques. In Computer Aided Verification - 29th International Conference , CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. 68\u201394 . Xujie Si, Xin Zhang, Radu Grigore, and Mayur Naik. 2017. Maximum Satisfiability in Software Analysis: Applications and Techniques. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. 68\u201394."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_41_1","volume-title":"Binary Translation Using Peephole Superoptimizers. In USENIX Symposium on Operating Systems Design and Implementation (OSDI).","author":"Sorav Bansal Alex Aiken","year":"2008","unstructured":"Alex Aiken Sorav Bansal . 2008 . Binary Translation Using Peephole Superoptimizers. In USENIX Symposium on Operating Systems Design and Implementation (OSDI). Alex Aiken Sorav Bansal. 2008. Binary Translation Using Peephole Superoptimizers. In USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737960"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_59"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480915"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/351397.351414"},{"key":"e_1_3_2_1_47_1","unstructured":"H. S. Warren. 2002. Hacker\u2019s Delight. Addison-Wesley.  H. S. Warren. 2002. Hacker\u2019s Delight. Addison-Wesley."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_26"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_16"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"}],"event":{"name":"SPLASH '17: Conference on Systems, Programming, Languages, and Applications: Software for Humanity","location":"Vancouver BC Canada","acronym":"SPLASH '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133850.3133856","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133850.3133856","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:34Z","timestamp":1750217434000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133850.3133856"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,25]]},"references-count":48,"alternative-id":["10.1145\/3133850.3133856","10.1145\/3133850"],"URL":"https:\/\/doi.org\/10.1145\/3133850.3133856","relation":{},"subject":[],"published":{"date-parts":[[2017,10,25]]},"assertion":[{"value":"2017-10-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}