{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:51Z","timestamp":1780994631385,"version":"3.54.1"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2012,8,2]],"date-time":"2012-08-02T00:00:00Z","timestamp":1343865600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10009-012-0249-7","type":"journal-article","created":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T17:50:25Z","timestamp":1343843425000},"page":"475-495","source":"Crossref","is-referenced-by-count":180,"title":["Program sketching"],"prefix":"10.1007","volume":"15","author":[{"given":"Armando","family":"Solar-Lezama","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2012,8,2]]},"reference":[{"key":"249_CR1","doi-asserted-by":"crossref","unstructured":"Amit, D., Rinetzky, N., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: In 19th International Conference on Computer Aided Verification (CAV) (2007)","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"249_CR2","unstructured":"Anderson, S.E.: Bit twiddling hacks (1997\u20132005). http:\/\/www-graphics.stanford.edu\/~seander\/bithacks.html"},{"issue":"3","key":"249_CR3","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1145\/356914.356918","volume":"15","author":"D. Angluin","year":"1983","unstructured":"Angluin D., Smith C.H.: Inductive inference: theory and methods. ACM Comput. Surv. 15(3), 237\u2013269 (1983)","journal-title":"ACM Comput. Surv."},{"key":"249_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A.: Resolve and expand. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, SAT\u201904, pp. 59\u201370. Springer, Berlin (2005)","DOI":"10.1007\/11527695_5"},{"issue":"5","key":"249_CR5","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke E., Grumberg O., Jha S., Lu Y., Veith H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"249_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D.,Yorav, K.: Behavioral consistency of c and verilog programs using bounded model checking. In: Proceedings of the 40th Annual Design Automation Conference, DAC \u201903, pp. 368\u2013371. ACM, New York (2003)","DOI":"10.1145\/775832.775928"},{"key":"249_CR7","unstructured":"Advanced Encryption Standard (AES): U.S. DEPARTMENT OF COMMERCE\/National Institute of Standards and Technology, November (2001). http:\/\/csrc.nist.gov\/publications\/fips\/fips197\/fips-197.pdf"},{"issue":"5","key":"249_CR8","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1016\/S0019-9958(67)91165-5","volume":"10","author":"E.M. Gold","year":"1967","unstructured":"Gold E.M.: Language identification in the limit. Inf. Control 10(5), 447\u2013474 (1967)","journal-title":"Inf. Control"},{"key":"249_CR9","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering, ICSE \u201910, vol. 1, pp. 215\u2013224. ACM, New York (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"249_CR10","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"249_CR11","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: Dag-aware AIG rewriting: a fresh look at combinational logic synthesis. In: DAC \u201906: Proceedings of the 43rd Annual Conference on Design Automation, pp. 532\u2013535. ACM Press, New York (2006)","DOI":"10.1145\/1146909.1147048"},{"key":"249_CR12","unstructured":"Ranjan, D.P., Tang, D., Malik, S.: A comparative study of 2qbf algorithms. In: The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), May (2004)"},{"key":"249_CR13","doi-asserted-by":"crossref","unstructured":"Samulowitz, H., Bacchus, F.: Binary clause reasoning in qbf. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing, SAT\u201906, pp. 353\u2013367. Springer, Berlin (2006)","DOI":"10.1007\/11814948_33"},{"key":"249_CR14","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: Cute: a concolic unit testing engine for c. In: ESEC\/SIGSOFT FSE, pp. 263\u2013272 (2005)","DOI":"10.21236\/ADA482657"},{"key":"249_CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1192.001.0001","volume-title":"Algorithmic Program Debugging","author":"E.Y. Shapiro","year":"1983","unstructured":"Shapiro E.Y.: Algorithmic Program Debugging. MIT Press, Cambridge (1983)"},{"key":"249_CR16","unstructured":"Solar-Lezama A.: Program Synthesis By Sketching. PhD thesis, EECS, UC Berkeley (2008)"},{"key":"249_CR17","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bod\u00edk, R., Saraswat, V., Seshia, S.: Sketching stencils. In: PLDI \u201907: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, vol. 42, pp. 167\u2013178. ACM, New York (2007)","DOI":"10.1145\/1250734.1250754"},{"key":"249_CR18","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C., Arnold, G., Bod\u00edk, R.: Sketching concurrent datastructures. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. Tucson, June 7\u201313 (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"249_CR19","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Saraswat, V., Seshia, S.: Combinatorial sketching for finite programs. In: ASPLOS\u201906. ACM Press, San Jose (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"249_CR20","doi-asserted-by":"crossref","DOI":"10.1145\/1706299.1706337","volume-title":"From program verification to program synthesis","author":"S. Srivastava","year":"2010","unstructured":"Srivastava S., Gulwani S., Foster J.: From program verification to program synthesis. POPL, Madrid (2010)"},{"issue":"1","key":"249_CR21","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1145\/321992.322002","volume":"24","author":"P.D. Summers","year":"1977","unstructured":"Summers P.D.: A methodology for lisp program construction from examples. J. ACM 24(1), 161\u2013175 (1977)","journal-title":"J. ACM"},{"key":"249_CR22","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. In: Bloem, R., Sharygina, N. (eds.) FMCAD, pp. 239\u2013246. IEEE (2010)"},{"key":"249_CR23","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 351\u2013363 (2005)","DOI":"10.1145\/1047659.1040334"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0249-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0249-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0249-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T12:23:17Z","timestamp":1743942197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0249-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,2]]},"references-count":23,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["249"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0249-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,2]]}}}