{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:04:20Z","timestamp":1776373460000,"version":"3.51.2"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030714994","type":"print"},{"value":"9783030715007","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Lifted<\/jats:italic> (<jats:italic>family-based<\/jats:italic>) <jats:italic>static analysis<\/jats:italic> by abstract interpretation is capable of analyzing all variants of a program family simultaneously, in a single run without generating any of the variants explicitly. The elements of the underlying lifted analysis domain are tuples, which maintain one property per variant. Still, explicit property enumeration in tuples, one by one for all variants, immediately yields combinatorial explosion. This is particularly apparent in the case of program families that, apart from Boolean features, contain also numerical features with large domains, thus giving rise to astronomical configuration spaces.<\/jats:p><jats:p>The key for an efficient lifted analysis is a proper handling of variability-specific constructs of the language (e.g., feature-based runtime tests and <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt {\\#if}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mrow>\n                      <mml:mo>#<\/mml:mo>\n                      <mml:mi>if<\/mml:mi>\n                    <\/mml:mrow>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> directives). In this work, we introduce a new symbolic representation of the lifted abstract domain that can efficiently analyze program families with numerical features. This makes sharing between property elements corresponding to different variants explicitly possible. The elements of the new lifted domain are constraint-based <jats:italic>decision trees<\/jats:italic>, where decision nodes are labeled with linear constraints defined over numerical features and the leaf nodes belong to an existing single-program analysis domain. To illustrate the potential of this representation, we have implemented an experimental lifted static analyzer, called <jats:sc>SPLNum<\/jats:sc><jats:inline-formula><jats:alternatives><jats:tex-math>$$^2$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:msup>\n                      <mml:mrow\/>\n                      <mml:mn>2<\/mml:mn>\n                    <\/mml:msup>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula><jats:sc>Analyzer<\/jats:sc>, for inferring invariants of C programs. An empirical evaluation on BusyBox and on benchmarks from SV-COMP yields promising preliminary results indicating that our decision trees-based approach is effective and outperforms the baseline tuple-based approach.<\/jats:p>","DOI":"10.1007\/978-3-030-71500-7_4","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T13:12:14Z","timestamp":1616159534000},"page":"67-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-2631","authenticated-orcid":false,"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3687-2233","authenticated-orcid":false,"given":"Sven","family":"Apel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2287-8925","authenticated-orcid":false,"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. Detection of feature interactions using feature-aware verification. In 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2011), pages 372\u2013375, 2011.","DOI":"10.1109\/ASE.2011.6100075"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Sven Apel, Alexander von Rhein, Philipp Wendler, Armin Gr\u00f6\u00dflinger, and Dirk Beyer. Strategies for product-line verification: case studies and experiments. In 35th Intern. Conference on Software Engineering, ICSE \u201913, pages 482\u2013491, 2013.","DOI":"10.1109\/ICSE.2013.6606594"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Claus Brabrand, M\u00e1rcio Ribeiro, T\u00e1rsis Tol\u00eado, Johnni Winther, and Paulo Borba. Intraprocedural dataflow analysis for software product lines. T. Aspect-Oriented Software Development, 10:73\u2013108, 2013.","DOI":"10.1007\/978-3-642-36964-3_3"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Junjie Chen and Patrick Cousot. A binary decision tree abstract domain functor. In Static Analysis - 22nd International Symposium, SAS 2015,Proceedings, volume 9291 of LNCS, pages 36\u201353. Springer, 2015.","DOI":"10.1007\/978-3-662-48288-9_3"},{"key":"4_CR5","unstructured":"Philipp Chrszon, Clemens Dubslaff, Sascha Kl\u00fcppelholz, and Christel Baier. Profeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput., 30(1):45\u201375, 2018."},{"key":"4_CR6","unstructured":"Paul Clements and Linda Northrop. Software Product Lines: Practices and Patterns. Addison-Wesley, 2001."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. 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 Principles of Programming Languages, pages 238\u2013252. ACM, 1977.","DOI":"10.1145\/512950.512973"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Patrick Cousot, Radhia Cousot, J\u00e9r\u00f4me Feret, Laurent Mauborgne, Antoine Min\u00e9, David Monniaux, and Xavier Rival. The astre\u00e9 analyzer. In Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Proceedings, volume 3444 of LNCS, pages 21\u201330. Springer, 2005.","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Patrick Cousot, Radhia Cousot, and Laurent Mauborgne. A scalable segmented decision tree abstract domain. In Time for Verification, Essays in Memory of Amir Pnueli, volume 6200 of LNCS, pages 72\u201395. Springer, 2010.","DOI":"10.1007\/978-3-642-13754-9_5"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (POPL\u201978), pages 84\u201396. ACM Press,1978.","DOI":"10.1145\/512760.512770"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Aleksandar\u00a0S. Dimovski. Lifted static analysis using a binary decision diagram abstract domain. In Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2019, pages 102\u2013114. ACM, 2019.","DOI":"10.1145\/3357765.3359518"},{"key":"4_CR12","unstructured":"Aleksandar\u00a0S. Dimovski. On calculating assertion probabilities for program families. Prilozi Contributions, Sec. Nat. Math. Biotech. Sci, MASA, 41(1):13\u201323, 2020."},{"key":"4_CR13","unstructured":"Aleksandar\u00a0S. Dimovski, Sven Apel, and Axel Legay. A decision tree lifted domain for analyzing program families with numerical features (extended version). CoRR, abs\/2012.05863, 2020."},{"key":"4_CR14","unstructured":"Aleksandar\u00a0S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Variability abstractions: Trading precision for speed in family-based analyses. In 29th European Conference on Object-Oriented Programming, ECOOP 2015, volume\u00a037 of LIPIcs, pages 247\u2013270. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2015."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Aleksandar\u00a0S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Finding suitable variability abstractions for lifted analysis. Formal Aspects Comput., 31(2):231\u2013259, 2019.","DOI":"10.1007\/s00165-019-00479-y"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Aleksandar\u00a0S. Dimovski and Axel Legay. Computing program reliability using forward-backward precondition analysis and model counting. In Fundamental Approaches to Software Engineering - 23rd International Conference, FASE 2020, Proceedings, volume 12076 of LNCS, pages 182\u2013202. Springer, 2020.","DOI":"10.1007\/978-3-030-45234-6_9"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Philippe Granger. Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 30(3-4):165\u2013190, 1989.","DOI":"10.1080\/00207168908803778"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Arie Gurfinkel and Sagar Chaki. Boxes: A symbolic abstract domain of boxes. In Static Analysis - 17th International Symposium, SAS 2010. Proceedings, volume 6337 of LNCS, pages 287\u2013303. Springer, 2010.","DOI":"10.1007\/978-3-642-15769-1_18"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Bertrand Jeannet and Antoine Min\u00e9. Apron: A library of numerical abstract domains for static analysis. In Computer Aided Verification, 21st Intern. Conference, CAV2009. Proceedings, volume 5643 of LNCS, pages 661\u2013667. Springer,2009.","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"4_CR20","unstructured":"Christian K\u00e4stner. Virtual Separation of Concerns: Toward Preprocessors 2.0. PhD thesis, University of Magdeburg, Germany, May 2010."},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Gary\u00a0A. Kildall. A unified approach to global program optimization. In Conference Record of the ACM Symposium on Principles of Programming Languages, (POPL\u201973), pages 194\u2013206, 1973.","DOI":"10.1145\/512927.512945"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Jan Midtgaard, Aleksandar\u00a0S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program., 105:145\u2013170, 2015.","DOI":"10.1016\/j.scico.2015.04.005"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Antoine Min\u00e9. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31\u2013100, 2006.","DOI":"10.1007\/s10990-006-8609-1"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Antoine Min\u00e9. Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages, 4(3-4):120\u2013372, 2017.","DOI":"10.1561\/2500000034"},{"key":"4_CR25","unstructured":"Daniel-Jesus Munoz, Jeho Oh, M\u00f3nica Pinto, Lidia Fuentes, and Don\u00a0S. Batory. Uniform random sampling product configurations of feature models that have numerical features. In Proceedings of the 23rd International Systems and Software Product Line Conference, SPLC 2019, Volume A, pages 39:1\u201339:13. ACM, 2019."},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Caterina Urban and Antoine Min\u00e9. A decision tree abstract domain for proving conditional termination. In Static Analysis - 21st International Symposium, SAS 2014.Proceedings, volume 8723 of LNCS, pages 302\u2013318. Springer, 2014.","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"4_CR27","unstructured":"Alexander von Rhein, J\u00f6rg Liebig, Andreas Janker, ChristianK\u00e4stner, and Sven Apel. Variability-aware static analysis at scale: An empirical study. ACM Trans. Softw. Eng. Methodol., 27(4):18:1\u201318:33, 2018."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71500-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:13:38Z","timestamp":1616199218000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71500-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030714994","9783030715007"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71500-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/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":"52","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":"16","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":"31% - 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":"5,5","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)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}