{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T23:14:36Z","timestamp":1761174876722,"version":"build-2065373602"},"reference-count":51,"publisher":"Polish Information Processing Society","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.15439\/2025f8874","type":"proceedings-article","created":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T07:44:23Z","timestamp":1761119063000},"page":"519-530","source":"Crossref","is-referenced-by-count":0,"title":["While-guard Synthesis by Abstract Static Analysis and CHC Solving"],"prefix":"10.15439","volume":"43","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-2631","authenticated-orcid":true,"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[{"name":"Mother Teresa University, Skopje"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"6175","published-online":{"date-parts":[[2025,10,15]]},"reference":[{"key":"ref1","doi-asserted-by":"publisher","unstructured":"A. Pnueli and R. Rosner, \u201cOn the synthesis of a reactive module,\u201d\nin Conference Record of the Sixteenth Annual ACM Symposium\non Principles of Programming Languages. ACM Press, 1989, pp.\n179\u2013190. [Online]. Available: https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"ref2","doi-asserted-by":"publisher","unstructured":"A. Solar-Lezama, \u201cProgram sketching,\u201d STTT, vol. 15, no. 5-6, pp. 475\u2013495, 2013. [Online]. Available: https:\/\/doi.org\/10.1007\/s10009-012-0249-7","DOI":"10.1007\/s10009-012-0249-7"},{"key":"ref3","doi-asserted-by":"publisher","unstructured":"A. Solar-Lezama, R. M. Rabbah, R. Bod\u00edk, and K. Ebcioglu,\n\u201cProgramming by sketching for bit-streaming programs,\u201d in Proceedings\nof the ACM SIGPLAN 2005 Conference on Programming Language\nDesign and Implementation. ACM, 2005, pp. 281\u2013294. [Online].\nAvailable: https:\/\/doi.org\/10.1145\/1065010.1065045","DOI":"10.1145\/1065010.1065045"},{"key":"ref4","doi-asserted-by":"publisher","unstructured":"A. Dimovski, S. Apel, and A. Legay, \u201cProgram sketching using lifted\nanalysis for numerical program families,\u201d in NASA Formal Methods,\nNFM 2021, ser. LNCS, vol. 12673. Springer, 2021, pp. 95\u2013112.\n[Online]. Available: https:\/\/doi.org\/10.1007\/978-3-030-76384-8_7","DOI":"10.1007\/978-3-030-76384-8_7"},{"key":"ref5","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski, \u201cGeneralized program sketching by abstract\ninterpretation and logical abduction,\u201d in Static Analysis - 30th\nInternational Symposium, SAS 2023, Proceedings, ser. LNCS, vol.\n14284. Springer, 2023, pp. 212\u2013230. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-031-44245-2_11","DOI":"10.1007\/978-3-031-44245-2_11"},{"key":"ref6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, \u201cAbstract interpretation: A unified lattice\nmodel for static analysis of programs by construction or approximation\nof fixpoints,\u201d in POPL\u201977. ACM, 1977, pp. 238\u2013252. [Online].\nAvailable: http:\/\/doi.acm.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"ref7","doi-asserted-by":"publisher","unstructured":"A. Min\u00e9, \u201cTutorial on static inference of numeric invariants by\nabstract interpretation,\u201d Foundations and Trends in Programming\nLanguages, vol. 4, no. 3-4, pp. 120\u2013372, 2017. [Online]. Available:\nhttps:\/\/doi.org\/10.1561\/2500000034","DOI":"10.1561\/2500000034"},{"key":"ref8","doi-asserted-by":"publisher","unstructured":"C. Urban and A. Min\u00e9, \u201cA decision tree abstract domain\nfor proving conditional termination,\u201d in Static Analysis - 21st\nInternational Symposium, SAS 2014. Proceedings, ser. LNCS,\nvol. 8723. Springer, 2014, pp. 302\u2013318. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-319-10936-7_19","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"ref9","doi-asserted-by":"publisher","unstructured":"I. Dillig and T. Dillig, \u201cExplain: A tool for performing\nabductive inference,\u201d in Computer Aided Verification - 25th\nInternational Conference, CAV 2013. Proceedings, ser. LNCS,\nvol. 8044. Springer, 2013, pp. 684\u2013689. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_46","DOI":"10.1007\/978-3-642-39799-8_46"},{"key":"ref10","doi-asserted-by":"publisher","unstructured":"A. Komuravelli, A. Gurfinkel, and S. Chaki, \u201cSmt-based model\nchecking for recursive programs,\u201d in Computer Aided Verification\n- 26th International Conference, CAV 2014. Proceedings, ser.\nLNCS, vol. 8559. Springer, 2014, pp. 17\u201334. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"ref11","doi-asserted-by":"publisher","unstructured":"H. Hojjat and P. R\u00fcmmer, \u201cThe ELDARICA horn solver,\u201d in 2018\nFormal Methods in Computer Aided Design, FMCAD 2018. IEEE,\n2018, pp. 1\u20137. [Online]. Available: https:\/\/doi.org\/10.23919\/FMCAD.\n2018.8603013","DOI":"10.23919\/FMCAD"},{"key":"ref12","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare and N. Wirth, \u201cAn axiomatic definition of the programming language PASCAL,\u201d Acta Informatica, vol. 2, pp. 335\u2013355, 1973.","DOI":"10.1007\/BF00289504"},{"key":"ref13","doi-asserted-by":"publisher","unstructured":"A. Min\u00e9, \u201cThe octagon abstract domain,\u201d Higher-Order and Symbolic\nComputation, vol. 19, no. 1, pp. 31\u2013100, 2006. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/s10990-006-8609-1","DOI":"10.1007\/s10990-006-8609-1"},{"key":"ref14","doi-asserted-by":"publisher","unstructured":"P. Cousot and N. Halbwachs, \u201cAutomatic discovery of linear restraints\namong variables of a program,\u201d in Conference Record of the Fifth\nAnnual ACM Symposium on POPL\u201978. ACM Press, 1978, pp. 84\u201396.\n[Online]. Available: https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"ref15","doi-asserted-by":"publisher","unstructured":"N. S. Bj\u00f8rner, K. L. McMillan, and A. Rybalchenko, \u201cOn\nsolving universally quantified horn clauses,\u201d in Static Analysis -\n20th International Symposium, SAS 2013. Proceedings, ser. LNCS,\nvol. 7935. Springer, 2013, pp. 105\u2013125. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-642-38856-9_8","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"ref16","doi-asserted-by":"publisher","unstructured":"G. Fedyukovich, S. Prabhu, K. Madhukar, and A. Gupta, \u201cQuantified\ninvariants via syntax-guided synthesis,\u201d in Computer Aided Verification\n- 31st International Conference, CAV 2019, Proceedings, Part I, ser.\nLNCS, vol. 11561. Springer, 2019, pp. 259\u2013277. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-030-25540-4_14","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"ref17","doi-asserted-by":"publisher","unstructured":"B. Jeannet and A. Min\u00e9, \u201cApron: A library of numerical abstract\ndomains for static analysis,\u201d in 21st Int. Conf., CAV 2009. Proceedings,\nser. LNCS, vol. 5643. Springer, 2009, pp. 661\u2013667. [Online].\nAvailable: https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"ref18","doi-asserted-by":"publisher","unstructured":"L. M. de Moura and N. Bj\u00f8rner, \u201cZ3: an efficient SMT solver,\u201d\nin 14th International Conference, TACAS 2008. Proceedings, ser.\nLNCS, vol. 4963. Springer, 2008, pp. 337\u2013340. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref19","doi-asserted-by":"publisher","unstructured":"I. Dillig, T. Dillig, B. Li, and K. L. McMillan, \u201cInductive invariant\ngeneration via abductive inference,\u201d in Proceedings of the 2013 ACM\nSIGPLAN International Conference on Object Oriented Programming\nSystems Languages & Applications, OOPSLA 2013. ACM, 2013, pp.\n443\u2013456. [Online]. Available: https:\/\/doi.org\/10.1145\/2509136.2509511","DOI":"10.1145\/2509136.2509511"},{"key":"ref20","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski, \u201cQuantitative program sketching using lifted static\nanalysis,\u201d in 25th Int. Conf. FASE 2022, Proceedings, ser. LNCS,\nvol. 13241. Springer, 2022, pp. 102\u2013122. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-030-99429-7_6","DOI":"10.1007\/978-3-030-99429-7_6"},{"key":"ref21","doi-asserted-by":"publisher","unstructured":"A. Dimovski, \u201cQuantitative program sketching using decision tree-based\nlifted analysis,\u201d J. Comput. Lang., vol. 75, p. 101206, 2023. [Online].\nAvailable: https:\/\/doi.org\/10.1016\/j.cola.2023.101206","DOI":"10.1016\/j.cola.2023.101206"},{"key":"ref22","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski, \u201cA binary decision diagram lifted domain for\nanalyzing program families,\u201d J. Comput. Lang., vol. 63, p. 101032,\n2021. [Online]. Available: https:\/\/doi.org\/10.1016\/j.cola.2021.101032","DOI":"10.1016\/j.cola.2021.101032"},{"key":"ref23","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski, S. Apel, and A. Legay, \u201cSeveral lifted abstract\ndomains for static analysis of numerical program families,\u201d Sci.\nComput. Program., vol. 213, p. 102725, 2022. [Online]. Available:\nhttps:\/\/doi.org\/10.1016\/j.scico.2021.102725","DOI":"10.1016\/j.scico.2021.102725"},{"key":"ref24","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski, C. Brabrand, and A. Wasowski, \u201cFinding suitable\nvariability abstractions for family-based analysis,\u201d in FM 2016:\nFormal Methods - 21st International Symposium, Proceedings, ser.\nLNCS, vol. 9995. Springer, 2016, pp. 217\u2013234. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_14","DOI":"10.1007\/978-3-319-48989-6_14"},{"key":"ref25","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski and A. Wasowski, \u201cFrom transition systems\nto variability models and from lifted model checking back to\nUPPAAL,\u201d in Models, Algorithms, Logics and Tools, ser. LNCS,\nvol. 10460. Springer, 2017, pp. 249\u2013268. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-319-63121-9_13","DOI":"10.1007\/978-3-319-63121-9_13"},{"key":"ref26","doi-asserted-by":"publisher","unstructured":"B. Atanasovski, M. Bogdanovic, G. Velinov, L. Stoimenov, A. S.\nDimovski, B. Koteska, D. Jankovic, I. Skrceska, M. Kon-Popovska, and\nB. Jakimovski, \u201cOn defining a model driven architecture for an enterprise\ne-health system,\u201d Enterp. Inf. Syst., vol. 12, no. 8-9, pp. 915\u2013941, 2018.\n[Online]. Available: https:\/\/doi.org\/10.1080\/17517575.2018.1521996","DOI":"10.1080\/17517575.2018.1521996"},{"key":"ref27","doi-asserted-by":"publisher","unstructured":"T. Dillig, I. Dillig, and S. Chaudhuri, \u201cOptimal guard synthesis for\nmemory safety,\u201d in Computer Aided Verification - 26th International\nConference, CAV 2014. Proceedings, ser. LNCS, vol. 8559. Austria:\nSpringer, 2014, pp. 491\u2013507. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-319-08867-9_32","DOI":"10.1007\/978-3-319-08867-9_32"},{"key":"ref28","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski, \u201cOn synthesizing presence conditions in numerical\nsoftware product lines,\u201d in Proceedings of the 29th ACM International\nSystems and Software Product Line Conference - Volume A, SPLC\n2025. ACM, 2025. [Online]. Available: https:\/\/doi.org\/10.1145\/3744915.3748474","DOI":"10.1145\/3744915.3748474"},{"key":"ref29","doi-asserted-by":"publisher","unstructured":"A. Albarghouthi, I. Dillig, and A. Gurfinkel, \u201cMaximal specification\nsynthesis,\u201d in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL\n2016. St. Petersburg: ACM, 2016, pp. 789\u2013801. [Online]. Available:\nhttps:\/\/doi.org\/10.1145\/2837614.2837628","DOI":"10.1145\/2837614.2837628"},{"key":"ref30","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski, \u201cWeakest safe context synthesis by symbolic\ngame semantics and logical abduction,\u201d in Proceedings of the 40th\nACM\/SIGAPP Symposium on Applied Computing, SAC 2025. ACM,\n2025, pp. 1990\u20131997. [Online]. Available: https:\/\/doi.org\/10.1145\/3672608.3707849","DOI":"10.1145\/3672608.3707849"},{"key":"ref31","doi-asserted-by":"publisher","unstructured":"F. Bourdoncle, \u201cAbstract debugging of higher-order imperative\nlanguages,\u201d in Proceedings of the ACM SIGPLAN\u201993 Conference on\nProgramming Language Design and Implementation (PLDI). ACM,\n1993, pp. 46\u201355. [Online]. Available: https:\/\/doi.org\/10.1145\/155090.155095","DOI":"10.1145\/155090.155095"},{"key":"ref32","doi-asserted-by":"publisher","unstructured":"A. Min\u00e9, \u201cBackward under-approximations in numeric abstract\ndomains to automatically infer sufficient program conditions,\u201d Sci.\nComput. Program., vol. 93, pp. 154\u2013182, 2014. [Online]. Available:\nhttps:\/\/doi.org\/10.1016\/j.scico.2013.09.014","DOI":"10.1016\/j.scico.2013.09.014"},{"key":"ref33","doi-asserted-by":"publisher","unstructured":"P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, D. Monniaux,\nand X. Rival, \u201cThe astre\u00e9 analyzer,\u201d in Programming Languages and\nSystems, 14th European Symposium on Programming, ESOP 2005,\nProceedings, ser. LNCS, vol. 3444. Springer, 2005, pp. 21\u201330.\n[Online]. Available: https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"ref34","doi-asserted-by":"publisher","unstructured":"M. Greitschus, D. Dietsch, M. Heizmann, A. Nutz, C. Sch\u00e4tzle,\nC. Schilling, F. Sch\u00fcssele, and A. Podelski, \u201cUltimate taipan: Trace\nabstraction and abstract interpretation - (competition contribution),\u201d\nin 23rd International Conference, TACAS 2017, Proceedings, Part\nII, ser. LNCS, vol. 10206, 2017, pp. 399\u2013403. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-662-54580-5_31","DOI":"10.1007\/978-3-662-54580-5_31"},{"key":"ref35","doi-asserted-by":"publisher","unstructured":"J. Henry, D. Monniaux, and M. Moy, \u201cPAGAI: A path sensitive static\nanalyser,\u201d Electron. Notes Theor. Comput. Sci., vol. 289, pp. 15\u201325,\n2012. [Online]. Available: https:\/\/doi.org\/10.1016\/j.entcs.2012.11.003","DOI":"10.1016\/j.entcs.2012.11.003"},{"key":"ref36","doi-asserted-by":"publisher","unstructured":"X. Rival, \u201cUnderstanding the origin of alarms in astr\u00e9e,\u201d in Static\nAnalysis, 12th International Symposium, SAS 2005, Proceedings, ser.\nLNCS, vol. 3672. Springer, 2005, pp. 303\u2013319. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/11547662_21","DOI":"10.1007\/11547662_21"},{"key":"ref37","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski and A. Legay, \u201cComputing program reliability\nusing forward-backward precondition analysis and model counting,\u201d in\nFundamental Approaches to Software Engineering - 23rd International\nConference, FASE 2020, Proceedings, ser. LNCS, vol. 12076.\nSpringer, 2020, pp. 182\u2013202. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-030-45234-6_9","DOI":"10.1007\/978-3-030-45234-6_9"},{"key":"ref38","doi-asserted-by":"crossref","unstructured":"R. Alur, R. Bod\u00edk, G. Juniwal, M. M. K. Martin, M. Raghothaman,\nS. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa,\n\u201cSyntax-guided synthesis,\u201d in Formal Methods in Computer-Aided\nDesign, FMCAD 2013. IEEE, 2013, pp. 1\u20138. [Online]. Available:\nhttp:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"ref39","doi-asserted-by":"publisher","unstructured":"Y. Gu, T. Tsukada, and H. Unno, \u201cOptimal CHC solving via termination\nproofs,\u201d Proc. ACM Program. Lang., vol. 7, no. POPL, pp. 604\u2013631,\n2023. [Online]. Available: https:\/\/doi.org\/10.1145\/3571214","DOI":"10.1145\/3571214"},{"key":"ref40","doi-asserted-by":"publisher","unstructured":"T. A. Beyene, C. Popeea, and A. Rybalchenko, \u201cSolving existentially\nquantified horn clauses,\u201d in Computer Aided Verification - 25th\nInternational Conference, CAV 2013. Proceedings, ser. LNCS, vol.\n8044. Springer, 2013, pp. 869\u2013882. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-642-39799-8_61","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"ref41","doi-asserted-by":"publisher","unstructured":"T. Kuwahara, R. Sato, H. Unno, and N. Kobayashi, \u201cPredicate\nabstraction and CEGAR for disproving termination of higherorder functional programs,\u201d in Computer Aided Verification - 27th\nInternational Conference, CAV 2015, Proceedings, Part II, ser.\nLNCS, vol. 9207. Springer, 2015, pp. 287\u2013303. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-319-21668-3_17","DOI":"10.1007\/978-3-319-21668-3_17"},{"key":"ref42","doi-asserted-by":"publisher","unstructured":"A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas, \u201cThe\nseahorn verification framework,\u201d in Computer Aided Verification -\n27th International Conference, CAV 2015, Proceedings, Part I, ser.\nLNCS, vol. 9206. Springer, 2015, pp. 343\u2013361. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"ref43","doi-asserted-by":"publisher","unstructured":"T. Kahsai, P. R\u00fcmmer, H. Sanchez, and M. Sch\u00e4f, \u201cJayhorn:\nA framework for verifying java programs,\u201d in Computer Aided\nVerification - 28th International Conference, CAV 2016, Proceedings,\nPart I, ser. LNCS, vol. 9779. Springer, 2016, pp. 352\u2013358. [Online].\nAvailable: https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"ref44","doi-asserted-by":"publisher","unstructured":"K. Hashimoto and H. Unno, \u201cRefinement type inference via horn\nconstraint optimization,\u201d in Static Analysis - 22nd International\nSymposium, SAS 2015, Saint-Malo, France, September 9-11, 2015,\nProceedings, ser. Lecture Notes in Computer Science, vol. 9291.\nSpringer, 2015, pp. 199\u2013216. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-662-48288-9_12","DOI":"10.1007\/978-3-662-48288-9_12"},{"key":"ref45","doi-asserted-by":"publisher","unstructured":"J. Leroux, P. R\u00fcmmer, and P. Subotic, \u201cGuiding craig\ninterpolation with domain-specific abstractions,\u201d Acta Informatica,\nvol. 53, no. 4, pp. 387\u2013424, 2016. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/s00236-015-0236-z","DOI":"10.1007\/s00236-015-0236-z"},{"key":"ref46","doi-asserted-by":"publisher","unstructured":"T. A. Beyene, S. Chaudhuri, C. Popeea, and A. Rybalchenko, \u201cA\nconstraint-based approach to solving games on infinite graphs,\u201d in\nThe 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles\nof Programming Languages, POPL \u201914. ACM, 2014, pp. 221\u2013234.\n[Online]. Available: https:\/\/doi.org\/10.1145\/2535838.2535860","DOI":"10.1145\/2535838.2535860"},{"key":"ref47","doi-asserted-by":"publisher","unstructured":"J. Kim, Q. Hu, L. D\u2019Antoni, and T. W. Reps, \u201cSemantics-guided\nsynthesis,\u201d Proc. ACM Program. Lang., vol. 5, no. POPL, pp. 1\u201332,\n2021. [Online]. Available: https:\/\/doi.org\/10.1145\/3434311","DOI":"10.1145\/3434311"},{"key":"ref48","doi-asserted-by":"publisher","unstructured":"K. J. C. Johnson, A. Reynolds, T. W. Reps, and L. D\u2019Antoni,\n\u201cThe semgus toolkit,\u201d in Computer Aided Verification - 36th\nInternational Conference, CAV 2024, Proceedings, Part III, ser.\nLNCS, vol. 14683. Springer, 2024, pp. 27\u201340. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-031-65633-0_2","DOI":"10.1007\/978-3-031-65633-0_2"},{"key":"ref49","doi-asserted-by":"publisher","unstructured":"S. So and H. Oh, \u201cSynthesizing imperative programs from\nexamples guided by static analysis,\u201d in Static Analysis - 24th\nInternational Symposium, SAS 2017, Proceedings, ser. LNCS,\nvol. 10422. Springer, 2017, pp. 364\u2013381. [Online]. Available:\nhttps:\/\/doi.org\/10.1007\/978-3-319-66706-5_18","DOI":"10.1007\/978-3-319-66706-5_18"},{"key":"ref50","doi-asserted-by":"publisher","unstructured":"A. S. Dimovski, \u201cImperative program synthesis by abstract static\nanalysis and SMT mutations,\u201d in Proceedings of the 24th ACM\nSIGPLAN International Conference on Generative Programming:\nConcepts and Experiences, GPCE 2025, Bergen, Norway, July\n3-4, 2025. ACM, 2025, pp. 27\u201340. [Online]. Available: https:\/\/doi.org\/10.1145\/3742876.3742884","DOI":"10.1145\/3742876.3742884"},{"key":"ref51","doi-asserted-by":"publisher","unstructured":"A. Dimovski, \u201cMutation-based lifted repair of software product\nlines,\u201d in 38th European Conference on Object-Oriented Programming,\nECOOP 2024, ser. LIPIcs, vol. 313. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2024, pp. 12:1\u201312:24. [Online]. Available:\nhttps:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2024.12","DOI":"10.4230\/LIPIcs.ECOOP.2024.12"}],"event":{"name":"20th Conference on Computer Science and Intelligence Systems (FedCSIS)","theme":"Computer Science and Intelligence Systems","location":"Krak\u00f3w, Poland","acronym":"FedCSIS","number":"20","start":{"date-parts":[[2025,9,14]]},"end":{"date-parts":[[2025,9,17]]}},"container-title":["Annals of Computer Science and Information Systems","Proceedings of the 20th Conference on Computer Science and Intelligence Systems (FedCSIS)"],"original-title":[],"deposited":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T07:49:14Z","timestamp":1761119354000},"score":1,"resource":{"primary":{"URL":"https:\/\/annals-csis.org\/Volume_43\/drp\/8874.html"}},"subtitle":[],"proceedings-subject":"Computer Science and Information Systems","short-title":[],"issued":{"date-parts":[[2025,10,15]]},"references-count":51,"URL":"https:\/\/doi.org\/10.15439\/2025f8874","relation":{},"ISSN":["2300-5963"],"issn-type":[{"value":"2300-5963","type":"print"}],"subject":[],"published":{"date-parts":[[2025,10,15]]}}}