{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:02:54Z","timestamp":1773478974578,"version":"3.50.1"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031442445","type":"print"},{"value":"9783031442452","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-44245-2_11","type":"book-chapter","created":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T15:02:30Z","timestamp":1698073350000},"page":"212-230","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Generalized Program Sketching by\u00a0Abstract Interpretation and\u00a0Logical Abduction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-2631","authenticated-orcid":false,"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,10,24]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 789\u2013801. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837628","DOI":"10.1145\/2837614.2837628"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, pp. 1\u20138. IEEE (2013). https:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation (PLDI), pp. 46\u201355. ACM (1993). https:\/\/doi.org\/10.1145\/155090.155095","DOI":"10.1145\/155090.155095"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 289\u2013300. ACM (2009). https:\/\/doi.org\/10.1145\/1480881.1480917","DOI":"10.1145\/1480881.1480917"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on POPL, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973. https:\/\/doi.acm.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P., et al.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21\u201330. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on POPL 1978, pp. 84\u201396. ACM Press (1978). https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1007\/978-3-642-39799-8_46","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2013","unstructured":"Dillig, I., Dillig, T.: Explain: a tool for performing abductive inference. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 684\u2013689. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_46"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-02658-4_20","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2009","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 233\u2013247. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_20"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, pp. 181\u2013192. ACM (2012). https:\/\/doi.org\/10.1145\/2254064.2254087","DOI":"10.1145\/2254064.2254087"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, pp. 443\u2013456. ACM (2013). https:\/\/doi.org\/10.1145\/2509136.2509511","DOI":"10.1145\/2509136.2509511"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-319-08867-9_32","volume-title":"Computer Aided Verification","author":"T Dillig","year":"2014","unstructured":"Dillig, T., Dillig, I., Chaudhuri, S.: Optimal guard synthesis for memory safety. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 491\u2013507. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_32"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S.: A binary decision diagram lifted domain for analyzing program families. J. Comput. Lang. 63, 101032 (2021)","DOI":"10.1016\/j.cola.2021.101032"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Lifted termination analysis by abstract interpretation and its applications. In: GPCE 2021: Concepts and Experiences, pp. 96\u2013109. ACM (2021). https:\/\/doi.org\/10.1145\/3486609.3487202","DOI":"10.1145\/3486609.3487202"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-030-99429-7_6","volume-title":"Fundamental Approaches to Software Engineering","author":"AS Dimovski","year":"2022","unstructured":"Dimovski, A.S.: Quantitative program sketching using lifted static analysis. In: FASE 2022. LNCS, vol. 13241, pp. 102\u2013122. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_6"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S.: Artifact for the paper \u201cgeneralized program sketching by abstract interpretation and logical abduction\u201d. Zenodo (2023)","DOI":"10.1007\/978-3-031-44245-2_11"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S.: Quantitative program sketching using decision tree-based lifted analysis. J. Comput. Lang. 75, 101206 (2023)","DOI":"10.1016\/j.cola.2023.101206"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Apel, S.: Lifted static analysis of dynamic program families by abstract interpretation. In: 35th European Conference on Object-Oriented Programming, ECOOP 2021. LIPIcs, vol. 194, pp. 14:1\u201314:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.14","DOI":"10.4230\/LIPIcs.ECOOP.2021.14"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-030-76384-8_7","volume-title":"NASA Formal Methods","author":"AS Dimovski","year":"2021","unstructured":"Dimovski, A.S., Apel, S., Legay, A.: Program sketching using lifted analysis for numerical program families. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 95\u2013112. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_7"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S., Apel, S., Legay, A.: Several lifted abstract domains for static analysis of numerical program families. Sci. Comput. Program. 213, 102725 (2022)","DOI":"10.1016\/j.scico.2021.102725"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-030-45234-6_9","volume-title":"Fundamental Approaches to Software Engineering","author":"AS Dimovski","year":"2020","unstructured":"Dimovski, A.S., Legay, A.: Computing program reliability using forward-backward precondition analysis and model counting. In: FASE 2020. LNCS, vol. 12076, pp. 182\u2013202. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_9"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-662-54580-5_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Greitschus","year":"2017","unstructured":"Greitschus, M., et al.: Ultimate taipan: trace abstraction and abstract interpretation. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 399\u2013403. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_31"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electron. Notes Theor. Comput. Sci. 289, 15\u201325 (2012)","DOI":"10.1016\/j.entcs.2012.11.003"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-36742-7_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Li","year":"2013","unstructured":"Li, B., Dillig, I., Dillig, T., McMillan, K., Sagiv, M.: Synthesis of circular compositional program proofs via abduction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 370\u2013384. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_26"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. High.-Order Symb. Comput. 19(1), 31\u2013100 (2006)","DOI":"10.1007\/s10990-006-8609-1"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Sci. Comput. Program. 93, 154\u2013182 (2014)","DOI":"10.1016\/j.scico.2013.09.014"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends Program. Lang. 4(3\u20134), 120\u2013372 (2017)","DOI":"10.1561\/2500000034"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11547662_21","volume-title":"Static Analysis","author":"X Rival","year":"2005","unstructured":"Rival, X.: Understanding the origin of alarms in Astr\u00e9e. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 303\u2013319. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_21"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-319-66706-5_18","volume-title":"Static Analysis","author":"S So","year":"2017","unstructured":"So, S., Oh, H.: Synthesizing imperative programs from examples guided by static analysis. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 364\u2013381. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_18"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013)","DOI":"10.1007\/s10009-012-0249-7"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, pp. 281\u2013294. ACM (2005). https:\/\/doi.org\/10.1145\/1065010.1065045","DOI":"10.1145\/1065010.1065045"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-319-10936-7_19","volume-title":"Static Analysis","author":"C Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 302\u2013318. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10936-7_19"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-030-32304-2_13","volume-title":"Static Analysis","author":"B Yin","year":"2019","unstructured":"Yin, B., Chen, L., Liu, J., Wang, J., Cousot, P.: Verifying numerical programs via iterative abstract testing. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 247\u2013267. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_13"},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Yoon, Y., Lee, W., Yi, K.: Inductive program synthesis via iterative forward-backward abstract interpretation. In: PLDI 2023: 44th ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 1657\u20131681. ACM (2023). https:\/\/doi.org\/10.1145\/3591288","DOI":"10.1145\/3591288"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-44245-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,8]],"date-time":"2024-02-08T08:15:06Z","timestamp":1707380106000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-44245-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031442445","9783031442452"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-44245-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"24 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2023","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":"sas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/sas-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}