{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T10:46:39Z","timestamp":1761129999003,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030994280"},{"type":"electronic","value":"9783030994297"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a novel approach for resolving numerical program sketches under Boolean and quantitative objectives. The input is a program sketch, which represents a partial program with missing numerical parameters (holes). The aim is to automatically synthesize values for the parameters, such that the resulting complete program satisfies: a <jats:italic>Boolean (qualitative) specification<\/jats:italic> given in the form of assertions; and a <jats:italic>quantitative specification<\/jats:italic> that estimates the number of execution steps to termination and which the synthesizer is expected to optimize.<\/jats:p><jats:p>To address the above quantitative sketching problem, we encode a program sketch as a program family (a.k.a. software product line) and analyze it by the specifically designed lifted analysis algorithms based on abstract interpretation. In particular, we use a combination of forward (numerical) and backward (termination) lifted analysis of program families to find the variants (family members) that satisfy all assertions, and moreover are optimal with respect to the given quantitative objective. Such obtained variants represent \u201ccorrect &amp; optimal\u201d sketch realizations.<\/jats:p><jats:p>We present a prototype implementation of our approach within the <jats:sc>FamilySketcher<\/jats:sc>\u00a0 tool for resolving C sketches with numerical types. We have evaluated our approach on a set of benchmarks, and experimental results confirm the effectiveness of our approach.<\/jats:p>","DOI":"10.1007\/978-3-030-99429-7_6","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"102-122","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Quantitative Program Sketching using Lifted Static Analysis"],"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":[[2022,3,29]]},"reference":[{"key":"6_CR1","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 2013. pp. 1\u20138. IEEE (2013), http:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Computer Aided Verification, 21st International Conference, CAV 2009. Proceedings. LNCS, vol. 5643, pp. 140\u2013156. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Bodden, E., Tol\u00eado, T., Ribeiro, M., Brabrand, C., Borba, P., Mezini, M.: Spl$${}^{\\text{lift}}$$: statically analyzing software product lines in minutes instead of years. In: ACM SIGPLAN Conference on PLDI \u201913. pp. 355\u2013364 (2013)","DOI":"10.1145\/2499370.2491976"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Ceska, M., Dehnert, C., Jansen, N., Junges, S., Katoen, J.: Model repair revamped: On the automated synthesis of markov chains. In: Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday. LNCS, vol. 11500, pp. 107\u2013125. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31514-6_7","DOI":"10.1007\/978-3-030-31514-6_7"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. In: Computer Aided Verification, 22nd International Conference, CAV 2010. Proceedings. LNCS, vol. 6174, pp. 380\u2013395. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_34","DOI":"10.1007\/978-3-642-14295-6_34"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Chaudhuri, S., Clochard, M., Solar-Lezama, A.: Bridging boolean and quantitative synthesis using smoothed proof search. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914. pp. 207\u2013220. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535859","DOI":"10.1145\/2535838.2535859"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Chen, J., Cousot, P.: A binary decision tree abstract domain functor. In: Static Analysis - 22nd International Symposium, SAS 2015, Proceedings. LNCS, vol. 9291, pp. 36\u201353. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_3","DOI":"10.1007\/978-3-662-48288-9_3"},{"key":"6_CR8","unstructured":"Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley (2001)"},{"key":"6_CR9","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: Conf. Record of the Fourth ACM Symposium on POPL. pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: A scalable segmented decision tree abstract domain. In: Time for Verification, Essays in Memory of Amir Pnueli. LNCS, vol. 6200, pp. 72\u201395. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-13754-9_5","DOI":"10.1007\/978-3-642-13754-9_5"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Lifted static analysis using a binary decision diagram abstract domain. In: Proceedings of the 18th ACM SIGPLAN International Conference on GPCE 2019. pp. 102\u2013114. ACM (2019). https:\/\/doi.org\/10.1145\/3357765.3359518","DOI":"10.1145\/3357765.3359518"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: A binary decision diagram lifted domain for analyzing program families. J. Comput. Lang. 63, 101032 (2021). https:\/\/doi.org\/10.1016\/j.cola.2021.101032","DOI":"10.1016\/j.cola.2021.101032"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Lifted termination analysis by abstract interpretation and its applications. In: GPCE \u201921: Concepts and Experiences, Chicago, IL, USA, October, 2021. pp. 96\u2013109. ACM (2021). https:\/\/doi.org\/10.1145\/3486609.3487202","DOI":"10.1145\/3486609.3487202"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Tool artifact for \u201cquantitative program sketching using lifted static analysis\u201d. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5898643, https:\/\/zenodo.org\/record\/5898643#.YhJLRejMLIU","DOI":"10.5281\/zenodo.5898643"},{"key":"6_CR15","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":"6_CR16","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S., Apel, S., Legay, A.: A decision tree lifted domain for analyzing program families with numerical features. In: Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Proceedings. LNCS, vol. 12649, pp. 67\u201386. Springer (2021), https:\/\/arxiv.org\/abs\/2012.05863","DOI":"10.1007\/978-3-030-71500-7_4"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Apel, S., Legay, A.: Program sketching using lifted analysis for numerical program families. In: NASA Formal Methods - 13th International Symposium, NFM 2021, Proceedings. LNCS, vol. 12673, pp. 95\u2013112. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_7","DOI":"10.1007\/978-3-030-76384-8_7"},{"key":"6_CR18","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1016\/j.scico.2021.102725","DOI":"10.1016\/j.scico.2021.102725"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions for lifted analysis. Sci. Comput. Program. 159, 1\u201327 (2018)","DOI":"10.1016\/j.scico.2017.12.012"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Brabrand, C., Wasowski, A.: Finding suitable variability abstractions for lifted analysis. Formal Aspects Comput. 31(2), 231\u2013259 (2019). https:\/\/doi.org\/10.1007\/s00165-019-00479-y","DOI":"10.1007\/s00165-019-00479-y"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Hunsen, C., Zhang, B., Siegmund, J., K\u00e4stner, C., Le\u00dfenich, O., Becker, M., Apel, S.: Preprocessor-based variability in open-source and industrial software systems: An empirical study. Empirical Software Engineering 21(2), 449\u2013482 (2016). https:\/\/doi.org\/10.1007\/s10664-015-9360-1","DOI":"10.1007\/s10664-015-9360-1"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Iosif-Lazar, A.F., Melo, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Effective analysis of C programs by rewriting variability. Art Sci. Eng. Program. 1(1), 1 (2017). https:\/\/doi.org\/10.22152\/programming-journal.org\/2017\/1\/1","DOI":"10.22152\/programming-journal.org\/2017\/1\/1"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Computer Aided Verification, 21st Inter. Conference, CAV 2009. Proceedings. LNCS, vol. 5643, pp. 661\u2013667. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Midtgaard, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program. 105, 145\u2013170 (2015). https:\/\/doi.org\/10.1016\/j.scico.2015.04.005","DOI":"10.1016\/j.scico.2015.04.005"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages 4(3-4), 120\u2013372 (2017). https:\/\/doi.org\/10.1561\/2500000034","DOI":"10.1561\/2500000034"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008. Proceedings. LNCS, vol. 4963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag, Secaucus, USA (1999)","DOI":"10.1007\/978-3-662-03811-6"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"von Rhein, A., Liebig, J., Janker, A., K\u00e4stner, C., Apel, S.: Variability-aware static analysis at scale: An empirical study. ACM Trans. Softw. Eng. Methodol. 27(4), 18:1\u201318:33 (2018). https:\/\/doi.org\/10.1145\/3280986","DOI":"10.1145\/3280986"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5-6), 475\u2013495 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0249-7","DOI":"10.1007\/s10009-012-0249-7"},{"key":"6_CR30","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":"6_CR31","unstructured":"Urban, C.: Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs. (Analyse Statique par Interpr\u00e9tation Abstraite de Propri\u00e9t\u00e9s Temporelles Fonctionnelles des Programmes). Ph.D. thesis, \u00c9cole Normale Sup\u00e9rieure, Paris, France (2015), https:\/\/tel.archives-ouvertes.fr\/tel-01176641"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: Static Analysis - 21st International Symposium, SAS 2014. Proceedings. LNCS, vol. 8723, pp. 302\u2013318. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-10936-7_19","DOI":"10.1007\/978-3-319-10936-7_19"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99429-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:16:56Z","timestamp":1648498616000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99429-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030994280","9783030994297"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99429-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","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":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"61","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":"17","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":"28% - 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","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":"7","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)"}}]}}