{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:40:01Z","timestamp":1750556401133,"version":"3.41.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_5","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"86-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis"],"prefix":"10.1007","author":[{"given":"Adri\u00e0","family":"Gasc\u00f3n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brent","family":"Carmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: 40th ACM Symposium Principles of Programming Languages POPL (2013)","DOI":"10.1145\/2429069.2429075"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD, pp. 1\u201317 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Kunz, C., Schmidt, B., Gregoire, B., Lakhnech, Y., Zanella-Beguelin, S.: Fully automated analysis of padding-based encryption in the computational model (2013). http:\/\/www.easycrypt.info\/zoocrypt\/","DOI":"10.1145\/2508859.2516663"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: A Tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). doi:10.1007\/978-3-319-10082-1_6"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-540-88313-5_13","volume-title":"Computer Security - ESORICS 2008","author":"D Bogdanov","year":"2008","unstructured":"Bogdanov, D., Laur, S., Willemson, J.: Sharemind: a framework for fast privacy-preserving computations. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 192\u2013206. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-88313-5_13"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/BFb0054851","volume-title":"Algorithmic Number Theory","author":"D Boneh","year":"1998","unstructured":"Boneh, D.: The decision Diffie-Hellman problem. In: Buhler, J.P. (ed.) ANTS 1998. LNCS, vol. 1423, pp. 48\u201363. Springer, Heidelberg (1998). doi:10.1007\/BFb0054851"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/978-3-662-53015-3_15","volume-title":"Advances in Cryptology \u2013 CRYPTO 2016","author":"B Carmer","year":"2016","unstructured":"Carmer, B., Rosulek, M.: Linicrypt: a model for practical cryptography. In: Robshaw, M., Katz, J. (eds.) CRYPTO 2016. LNCS, vol. 9816, pp. 416\u2013445. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-53015-3_15"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Chou, T., Orlandi, C.: The simplest protocol for oblivious transfer. Cryptology ePrint Archive, Report 2015\/267 (2015). http:\/\/eprint.iacr.org\/","DOI":"10.1007\/978-3-319-22174-8_3"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symposium on Principles of Programming Languages, POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-1-4615-1467-1_6","volume-title":"E-Commerce Security and Privacy","author":"W Du","year":"2001","unstructured":"Du, W., Atallah, M.J.: Protocols for secure remote database access with approximate matching. In: Ghosh, A.K. (ed.) E-Commerce Security and Privacy, pp. 87\u2013111. Springer, Heidelberg (2001)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Felgentreff, T., Millstein, T., Borning, A., Hirschfeld, R.: Checks and balances: constraint solving without surprises in object-constraint programming languages. In: Proceedings Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA (2015)","DOI":"10.1145\/2814270.2814311"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Frankle, J., Osera, P., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. In: POPL, pp. 802\u2013815. ACM (2016)","DOI":"10.1145\/2914770.2837629"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Gasc\u00f3n, A., Subramanyan, P., Dutertre, B., Tiwari, A., Jovanovic, D., Malik, S.: Template-based circuit understanding. In: Formal Methods in Computer-Aided Design, FMCAD, pp. 83\u201390. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987599"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Gasc\u00f3n, A., Tiwari, A.: Synudic: synthesis using dual interpretation on components (2016). https:\/\/github.com\/adriagascon\/synudic","DOI":"10.1007\/978-3-319-21401-6_33"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/3-540-48405-1_8","volume-title":"Advances in Cryptology \u2014 CRYPTO 1999","author":"N Gilboa","year":"1999","unstructured":"Gilboa, N.: Two party RSA key generation. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 116\u2013129. Springer, Heidelberg (1999). doi:10.1007\/3-540-48405-1_8"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proceedings of ACM Conference on Programing Language Design and Implementation PLDI, pp. 62\u201373 (2011)","DOI":"10.1145\/1993316.1993506"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings of ACM Conference on Programming Language Design and Implementation, PLDI, pp. 281\u2013292 (2008)","DOI":"10.1145\/1379022.1375616"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Hoang, V., Katz, J., Malozemoff, A.: Automated analysis and synthesis of authenticated encryption schemes. In: ACM CCS (2015)","DOI":"10.1145\/2810103.2813636"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings of ICSE, vol. 1, pp. 215\u2013224. ACM (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA, pp. 407\u2013426. ACM (2013)","DOI":"10.1145\/2544173.2509555"},{"key":"5_CR21","unstructured":"Lindell, Y.: How to simulate it - a tutorial on the simulation proof technique. Cryptology ePrint Archive, Report 2016\/046 (2016). http:\/\/eprint.iacr.org\/2016\/046"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Malozemoff, A.J., Katz, J., Green, M.D.: Automated analysis and synthesis of block-cipher modes of operation. In: IEEE 27th Computer Security Foundations Symposium, CSF, pp. 140\u2013152. IEEE (2014)","DOI":"10.1109\/CSF.2014.18"},{"issue":"3","key":"5_CR23","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/362566.362568","volume":"14","author":"Z Manna","year":"1971","unstructured":"Manna, Z., Waldinger, R.J.: Toward automatic program synthesis. Commun. ACM 14(3), 151\u2013165 (1971)","journal-title":"Commun. ACM"},{"key":"5_CR24","unstructured":"Microsoft Research: Z3: an efficient SMT solver. http:\/\/research.microsoft.com\/projects\/z3\/"},{"key":"5_CR25","unstructured":"Naor, M., Pinkas, B.: Efficient oblivious transfer protocols. In: Proceedings of 12th ACM-SIAM Symposium on Discrete Algorithms, SODA, pp. 448\u2013457 (2001)"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: PLDI, pp. 522\u2013538. ACM (2016)","DOI":"10.1145\/2980983.2908093"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Smith, C., Albarghouthi, A.: Mapreduce program synthesis. In: PLDI, pp. 326\u2013340. ACM (2016)","DOI":"10.1145\/2980983.2908102"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI (2005)","DOI":"10.1145\/1065010.1065045"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Saraswat, V., Seshia, S.: Combinatorial sketching for finite programs. In: ASPLOS (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"5_CR30","unstructured":"SRI International: Yices: an SMT solver. http:\/\/yices.csl.sri.com\/"},{"issue":"5\u20136","key":"5_CR31","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. STTT 15(5\u20136), 497\u2013518 (2013)","journal-title":"STTT"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-319-21401-6_33","volume-title":"Automated Deduction \u2013 CADE-25","author":"A Tiwari","year":"2015","unstructured":"Tiwari, A., Gasc\u00f3n, A., Dutertre, B.: Program synthesis using dual interpretation. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 482\u2013497. Springer, Cham (2015). doi:10.1007\/978-3-319-21401-6_33"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:06:24Z","timestamp":1750554384000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}