{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:14:01Z","timestamp":1743063241522,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030449131"},{"type":"electronic","value":"9783030449148"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"vor","delay-in-days":108,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Program sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the assertions. The most popular sketching tool, <jats:sc>Sketch<\/jats:sc>, can efficiently solve complex program sketches, but uses an integer encoding that often performs poorly if the sketched program manipulates large integer values. In this paper, we propose a new solving technique that allows <jats:sc>Sketch<\/jats:sc> to handle large integer values while retaining its integer encoding. Our technique uses a result from number theory, the Chinese Remainder Theorem, to rewrite program sketches to only track the remainders of certain variable values with respect to several prime numbers. We prove that our transformation is sound and the encoding of the resulting programs are exponentially more succinct than existing <jats:sc>Sketch<\/jats:sc> encodings. We evaluate our technique on a variety of benchmarks manipulating large integer values. Our technique provides speedups against both existing <jats:sc>Sketch<\/jats:sc> solvers and can solve benchmarks that existing <jats:sc>Sketch<\/jats:sc> solvers cannot handle.<\/jats:p>","DOI":"10.1007\/978-3-030-44914-8_21","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"572-598","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Solving Program Sketches with Large Integer Values"],"prefix":"10.1007","author":[{"given":"Rong","family":"Pan","sequence":"first","affiliation":[]},{"given":"Qinheping","family":"Hu","sequence":"additional","affiliation":[]},{"given":"Rishabh","family":"Singh","sequence":"additional","affiliation":[]},{"given":"Loris","family":"D\u2019Antoni","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"A.\u00a0Abate, C.\u00a0David, P.\u00a0Kesseli, D.\u00a0Kroening, and E.\u00a0Polgreen. Counterexample guided inductive synthesis modulo theories. In CAV, Lecture Notes in Computer Science. Springer, 2018.","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"R.\u00a0Alur, R.\u00a0Bod\u00edk, G.\u00a0Juniwal, M.\u00a0M.\u00a0K. Martin, M.\u00a0Raghothaman, S.\u00a0A. Seshia, R.\u00a0Singh, A.\u00a0Solar-Lezama, E.\u00a0Torlak, and A.\u00a0Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 1\u20138, 2013.","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"A.\u00a0Cheung, A.\u00a0Solar-Lezama, and S.\u00a0Madden. Optimizing database-backed applications with query synthesis. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, pages 3\u201314, 2013.","DOI":"10.1145\/2491956.2462180"},{"key":"21_CR4","unstructured":"L.\u00a0N. Childs, editor. The Chinese Remainder Theorem, pages 253\u2013281. Springer New York, New York, NY, 2009."},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"E.\u00a0M. Clarke, O.\u00a0Grumberg, and D.\u00a0E. Long. Model checking and abstraction. ACM Trans. Program. Lang. Syst., 16(5):1512\u20131542, Sept. 1994.","DOI":"10.1145\/186025.186051"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"P.\u00a0Cousot and R.\u00a0Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201977, pages 238\u2013252, New York, NY, USA, 1977. ACM.","DOI":"10.1145\/512950.512973"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"L.\u00a0D\u2019Antoni, R.\u00a0Samanta, and R.\u00a0Singh. Qlose: Program repair with quantitative objectives. In CAV (2), volume 9780 of Lecture Notes in Computer Science, pages 383\u2013401. Springer, 2016.","DOI":"10.1007\/978-3-319-41540-6_21"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"S.\u00a0de\u00a0Oliveira, S.\u00a0Bensalem, and V.\u00a0Prevosto. Polynomial invariants by linear algebra. In C.\u00a0Artho, A.\u00a0Legay, and D.\u00a0Peled, editors, Automated Technology for Verification and Analysis, pages 479\u2013494, Cham, 2016. Springer International Publishing.","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"P.\u00a0Dusart. Estimates of $$\\psi $$,$$\\vartheta $$ for large values of x without the riemann hypothesis. Math. Comput., 85(298):875\u2013888, 2016.","DOI":"10.1090\/mcom\/3005"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Feng, R.\u00a0Martins, J.\u00a0Van\u00a0Geffen, I.\u00a0Dillig, and S.\u00a0Chaudhuri. Component-based synthesis of table consolidation and transformation tasks from examples. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 422\u2013436, New York, NY, USA, 2017. ACM.","DOI":"10.1145\/3062341.3062351"},{"key":"21_CR11","unstructured":"J.\u00a0Grobchadl. The chinese remainder theorem and its application in a high-speed rsa crypto chip. In Proceedings of the 16th Annual Computer Security Applications Conference, ACSAC \u201900, pages 384\u2013, Washington, DC, USA, 2000. IEEE Computer Society."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"S.\u00a0Gulwani. Automating string processing in spreadsheets using input-output examples. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 317\u2013330, 2011.","DOI":"10.1145\/1925844.1926423"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"S.\u00a0Gulwani, W.\u00a0R. Harris, and R.\u00a0Singh. Spreadsheet data manipulation using examples. Commun. ACM, 55(8):97\u2013105, 2012.","DOI":"10.1145\/2240236.2240260"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"S.\u00a0Gulwani, O.\u00a0Polozov, and R.\u00a0Singh. Program synthesis. Foundations and Trends in Programming Languages, 4(1-2):1\u2013119, 2017.","DOI":"10.1561\/2500000010"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"G.\u00a0J.\u00a0O. Jameson. The Prime Number Theorem. London Mathematical Society Student Texts. Cambridge University Press, 2003.","DOI":"10.1017\/CBO9781139164986"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"N.\u00a0Polikarpova, I.\u00a0Kuraj, and A.\u00a0Solar-Lezama. Program synthesis from polymorphic refinement types. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 522\u2013538, 2016.","DOI":"10.1145\/2908080.2908093"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"R.\u00a0Singh and S.\u00a0Gulwani. Transforming spreadsheet data types using examples. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 343\u2013356, 2016.","DOI":"10.1145\/2837614.2837668"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"R.\u00a0Singh, S.\u00a0Gulwani, and A.\u00a0Solar-Lezama. Automated feedback generation for introductory programming assignments. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, June 16-19, 2013, pages 15\u201326, 2013.","DOI":"10.1145\/2499370.2462195"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"A.\u00a0Solar-Lezama. Program sketching. STTT, 15(5-6):475\u2013495, 2013.","DOI":"10.1007\/s10009-012-0249-7"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"A.\u00a0Solar-Lezama, C.\u00a0G. Jones, and R.\u00a0Bod\u00edk. Sketching concurrent data structures. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 136\u2013148, 2008.","DOI":"10.1145\/1379022.1375599"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"A.\u00a0Solar-Lezama, L.\u00a0Tancau, R.\u00a0Bodik, S.\u00a0Seshia, and V.\u00a0Saraswat. Combinatorial sketching for finite programs. SIGOPS Oper. Syst. Rev., 40(5):404\u2013415, Oct. 2006.","DOI":"10.1145\/1168917.1168907"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"A.\u00a0Tiwari, A.\u00a0Gasc\u00f3n, and B.\u00a0Dutertre. Program synthesis using dual interpretation. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 482\u2013497, 2015.","DOI":"10.1007\/978-3-319-21401-6_33"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"E.\u00a0Torlak and R.\u00a0Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201914, pages 530\u2013541, New York, NY, USA, 2014. ACM.","DOI":"10.1145\/2594291.2594340"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"A.\u00a0Udupa, A.\u00a0Raghavan, J.\u00a0V. Deshmukh, S.\u00a0Mador-Haim, M.\u00a0M. Martin, and R.\u00a0Alur. Transit: Specifying protocols with concolic snippets. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, pages 287\u2013296, 2013.","DOI":"10.1145\/2491956.2462174"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"X.\u00a0Wang, I.\u00a0Dillig, and R.\u00a0Singh. Program synthesis using abstraction refinement. PACMPL, 2(POPL):63:1\u201363:30, 2018.","DOI":"10.1145\/3158151"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"S.-M. Yen, S.\u00a0Kim, S.\u00a0Lim, and S.-J. Moon. Rsa speedup with chinese remainder theorem immune against hardware fault cryptanalysis. IEEE Trans. Comput., 52(4):461\u2013472, Apr. 2003.","DOI":"10.1109\/TC.2003.1190587"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-44914-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T17:11:49Z","timestamp":1656609109000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-44914-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030449131","9783030449148"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44914-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11-12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}