{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T13:54:03Z","timestamp":1772200443156,"version":"3.50.1"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"The Danish Council for Independent Research under a Sapere Aude project","award":["0602-02327B"],"award-info":[{"award-number":["0602-02327B"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2019,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Many software systems are today variational: they are built as program families or Software Product Lines. They can produce a potentially huge number of related programs, known as products or variants, by selecting suitable configuration options (features) at compile time. Many such program families are safety critical, yet the appropriate tools only rarely are able to analyze them effeciently. Researchers have addressed this problem by designing specialized\n            <jats:italic>variability-aware<\/jats:italic>\n            static (dataflow) analyses, which allow analyzing all variants of the family, simultaneously, in a single run without generating any of the variants explicitly. They are also known as\n            <jats:italic>lifted<\/jats:italic>\n            or\n            <jats:italic>family-based<\/jats:italic>\n            analyses. They take as input the common code base, which encodes all variants of a program family, and produce precise analysis results corresponding to all variants. These analyses scale much better than \u201cbrute force\u201d approach, where all individual variants are analyzed in isolation, one-by-one, using off-the-shelf single-program analyzers. Nevertheless, the computational cost of lifted analyses still greatly depends on the number of features and variants (which is often huge). For families with a large number of features and variants, the lifted analyses may be too costly or even infeasible. In order to speed up lifted analyses and make them computationally cheaper, variability abstractions which simplify variability away from program families and lifted analyses have been introduced. However, the space of possible variability abstractions is still intractably large to search naively, with most abstractions being either too imprecise or too costly.\n          <\/jats:p>\n          <jats:p>\n            We introduce here a method to efficiently find suitable variability abstractions from a large space of possible abstractions for a lifted static analysis. The main idea is to use a\n            <jats:italic>pre-analysis<\/jats:italic>\n            to estimate the impact of variability-specific parts of the program family on the analysis\u2019s precision. The pre-analysis is fully variability-aware while it aggressively abstracts the other semantics aspects. Then we use the pre-analysis results to find out when and where the subsequent abstract lifted analysis should turn off or on its variability-awareness. The abstraction constructed in this way is effective in discarding variability-specific program details that are irrelevant for showing the analysis\u2019s ultimate goal. We formalize this approach and we illustrate its effectiveness on several Java case studies. The evaluation shows that our approach which consists of running a pre-analysis followed by a subsequent abstract lifted analysis achieves competitive the precision-speed tradeoff compared to the standard lifted analysis.\n          <\/jats:p>","DOI":"10.1007\/s00165-019-00479-y","type":"journal-article","created":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T20:29:28Z","timestamp":1552681768000},"page":"231-259","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Finding suitable variability abstractions for lifted analysis"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-2631","authenticated-orcid":false,"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[{"name":"Mother Teresa University, 12 Udarna Brigada 2a, 1000, Skopje, Macedonia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claus","family":"Brabrand","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Rued Langgaards Vej 7, 2300, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Wa\u0328sowski","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Rued Langgaards Vej 7, 2300, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2009.8.5.c5"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Batory D (2005) Feature models grammars and propositional formulas. In: 9th International software product lines conference SPLC '05 volume 3714 of LNCS Springer-Verlag pp 7\u201320","DOI":"10.1007\/11554844_3"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36964-3_3"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bodden E Tol\u00eado T Ribeiro M Brabrand C Borba P Mezini M (2013) Spllift: statically analyzing software product lines in minutes instead of years. In: ACM SIGPLAN conference on PLDI '13 pp 355\u2013364","DOI":"10.1145\/2499370.2491976"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"POPL'77","author":"Cousot P","year":"1977"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cousot P Cousot R (1979) Systematic design of program analysis frameworks. In: POPL'79 pp 269\u2013282","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Chen J Cousot P (2015) A binary decision tree abstract domain functor. In: Static analysis\u201422nd international symposium SAS 2015 Saint-Malo France September 9\u201311 2015 Proceedings volume 9291 of LNCS Springer pp 36\u201353","DOI":"10.1007\/978-3-662-48288-9_3"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0234-1"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Cousot P Cousot R Mauborgne L (2010) A scalable segmented decision tree abstract domain. In: Time for verification essays in memory of Amir Pnueli volume 6200 of LNCS Springer pp 72\u201395","DOI":"10.1007\/978-3-642-13754-9_5"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2012.86"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0432-4"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Chen S Erwig M Walkingshaw E (2012) An error-tolerant type system for variational lambda calculus. In: ACM SIGPLAN international conference on functional programming ICFP'12 pp 29\u201340","DOI":"10.1145\/2398856.2364535"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Classen A Heymans P Schobbens P-Y Legay A (2011) Symbolic model checking of software product lines. In: Proceedings of the 33rd international conference on software engineering ICSE 2011 pp 321\u2013330","DOI":"10.1145\/1985793.1985838"},{"key":"e_1_2_1_2_16_2","volume-title":"Software product lines: practices and patterns","author":"Clements P","year":"2001"},{"key":"e_1_2_1_2_17_2","first-page":"1","volume-title":"Calculational system design, NATO ASI series F","author":"Cousot P","year":"1999"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Chechik M Stavropoulou I Disenfeld C Rubin J (2018) FPH: efficient non-commutativity analysis of feature-based systems. In: Fundamental approaches to software engineering 21st international conference FASE 2018 proceedings. volume 10802 of LNCS Springer pp 319\u2013336","DOI":"10.1007\/978-3-319-89363-1_18"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Cordy M Schobbens P-Y Heymans P Legay A (2012) Behavioural modelling and verification of real-time software product lines. In: 16th International software product line conference SPLC '12 Vol 1. ACM pp 66\u201375","DOI":"10.1145\/2362536.2362549"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Dimovski AS Al-Sibahi AS Brabrand C Wasowski A (2015) Family-based model checking without a family-based model checker. In: Model checking software\u201422nd international symposium SPIN 2015 proceedings volume 9232 of LNCS Springer pp 282\u2013299","DOI":"10.1007\/978-3-319-23404-5_18"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0425-2"},{"key":"e_1_2_1_2_22_2","unstructured":"Dimovski AS Brabrand C Wasowski A (2015) Variability abstractions: trading precision for speed in family-based analyses. In: 29th European conference on object-oriented programming ECOOP 2015 volume\u00a037 of LIPIcs Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik pp 247\u2013270"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Dimovski AS Brabrand C Wasowski A (2016) Finding suitable variability abstractions for family-based analysis. In: FM 2016: formal methods\u201421st international symposium proceedings volume 9995 of LNCS pp 217\u2013234","DOI":"10.1007\/978-3-319-48989-6_14"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.12.012"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.01.016"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Dimovski AS (2016) Symbolic game semantics for model checking program families. In: Model checking software\u201423nd international symposium SPIN 2016 proceedings volume 9641 of LNCS Springer pp 19\u201337","DOI":"10.1007\/978-3-319-32582-8_2"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Dimovski AS (2018) Abstract family-based model checking using modal featured transition systems: preservation of . In: Fundamental approaches to software engineering 21st international conference FASE 2018 proceedings. volume 10802 of LNCS Springer pp 301\u2013318","DOI":"10.1007\/978-3-319-89363-1_17"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.09.029"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Dimovski AS Wasowski A (2017) From transition systems to variability models and from lifted model checking back to UPPAAL. In: Models algorithms logics and tools\u2014essays dedicated to kim guldstrand Larsen on the occasion of his 60th birthday volume 10460 of LNCS Springer pp 249\u2013268","DOI":"10.1007\/978-3-319-63121-9_13"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Dimovski AS Wasowski A (2017) Variability-specific abstraction refinement for family-based model checking. In: Fundamental approaches to software engineering\u201420th international conference FASE 2017 proceedings volume 10202 of LNCS pp 406\u2013423","DOI":"10.1007\/978-3-662-54494-5_24"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Erwig M Walkingshaw E (2011) The choice calculus: a representation for software variation. ACM Trans Softw Eng Methodol 21(1):6:1\u20136:27","DOI":"10.1145\/2063239.2063245"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Gazzillo P Grimm R (2012) Superc: parsing all of C by taming the preprocessor. In: Vitek J Lin H Tip F (eds) ACM SIGPLAN conference on programming language design and implementation PLDI '12 Beijing China\u2014June 11\u201316 2012 ACM pp 323\u2013334","DOI":"10.1145\/2345156.2254103"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Iosif-Lazar AF Al-Sibahi AS Dimovski AS Savolainen JE Sierszecki K Wasowski A (2015) Experiences from designing and validating a software modernization transformation (E). In: 30th IEEE\/ACM International conference on automated software engineering ASE 2015 pp 597\u2013607","DOI":"10.1109\/ASE.2015.84"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2017\/1\/1"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Jeannet B Min\u00e9 A (2009) Apron: a library of numerical abstract domains for static analysis. In: Computer aided verification 21st international conference CAV 2009. Proceedings volume 5643 of LNCS Springer pp 661\u2013667","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_2_1_2_36_2","unstructured":"Christian K Apel S (2008) Type-checking software product lines\u2014a formal approach. In: 23rd IEEE\/ACM international conference on automated software engineering (ASE) 2008) pp 258\u2013267"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"K\u00e4stner C Apel S Kuhlemann M (2008) Granularity in software product lines. In: Proceedings of the 30th international conference on software engineering (ICSE'08) Leipzig Germany ACM pp 311\u2013320","DOI":"10.1145\/1368088.1368131"},{"key":"e_1_2_1_2_38_2","unstructured":"Kastner C (2010) Virtual separation of concerns: toward preprocessors 2.0. Ph.D. thesis University of Magdeburg Germany"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"K\u00e4stner C Giarrusso PG Rendel T Erdweg S Ostermann K Berger T (2011) Variability-aware parsing in the presence of lexical macros and conditional compilation. In: Proceedings of the 26th annual ACM SIGPLAN conference on object-oriented programming systems languages and applications OOPSLA 2011 part of SPLASH 2011 pp 805\u2013824","DOI":"10.1145\/2076021.2048128"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Larsen KG Nyman U Wasowski A (2007) Modal I\/O automata for interface and product line theories. In: Programming languages and systems 16th European symposium on programming ESOP 2007 proceedings volume 4421 of LNCS Springer pp 64\u201379","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Liang P Tripp O Naik M (2011) Learning minimal abstractions. In: Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL 2011 pp 31\u201342","DOI":"10.1145\/1926385.1926391"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.04.005"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Meinicke J Wong C-P K\u00e4stner C Th\u00fcm T Saake G (2016) On essential configuration complexity: measuring interactions in highly-configurable systems. In: Proceedings of the 31st IEEE\/ACM international conference on automated software engineering ASE 2016 Singapore September 3\u20137 2016 ACM pp 483\u2013494","DOI":"10.1145\/2970276.2970322"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Naik M Yang H Castelnuovo G Sagiv M (2012) Abstractions from tests. In: Proceedings of the 39th ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL 2012 pp 373\u2013386","DOI":"10.1145\/2103621.2103701"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Oh H Lee W Heo K Yang H Yi K (2014) Selective context-sensitivity guided by impact pre-analysis. In: ACM SIGPLAN conference on programming language design and implementation PLDI '14 p 49","DOI":"10.1145\/2594291.2594318"},{"issue":"2","key":"e_1_2_1_2_47_2","first-page":"6","article-title":"Selective x-sensitive analysis guided by impact pre-analysis","volume":"38","author":"Oh H","year":"2016","journal-title":"ACM Trans Program Lang Syst"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.02.024"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Reps T Horwitz S Sagiv M (1995) Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL '95 pp 49\u201361","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Scholz W Th\u00fcm T Apel S Lengauer C (2011) Automatic detection of feature interactions using the java modeling language: an experience report. In: Software product lines\u201415th international conference SPLC 2011 workshop proceedings Vol 2. ACM p 7","DOI":"10.1145\/2019136.2019144"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Th\u00fcm T Apel S K\u00e4stner C Schaefer I Saake G (2014) A classification and survey of analysis strategies for software product lines. ACM Comput Surv 47(1):6:1\u20136:45","DOI":"10.1145\/2580950"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.11.006"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Urban C Min\u00e9 A (2014) A decision tree abstract domain for proving conditional termination. In: Static analysis\u201421st international symposium SAS 2014. Proceedings volume 8723 of LNCS Springer pp 302\u2013318","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"e_1_2_1_2_55_2","unstructured":"von Rhein A (2016) Analysis strategies for configurable systems. Ph.D. thesis University of Passau Germany"},{"key":"e_1_2_1_2_56_2","unstructured":"Vall\u00e9e-Rai R Co P Gagnon E Hendren L Lam P Sundaresan V (1999) Soot\u2014a java bytecode optimization framework. In: Proceedings of the 1999 conference of the centre for advanced studies on collaborative research (CASCON'99) IBM Press pp 13"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"publisher","DOI":"10.5555\/151145"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Zhang X Naik M Yang H (2013) Finding optimum abstractions in parametric dataflow analysis. In: ACM SIGPLAN conference on programming language design and implementation PLDI '13 pp 365\u2013376","DOI":"10.1145\/2499370.2462185"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-019-00479-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-019-00479-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-019-00479-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-019-00479-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:57:52Z","timestamp":1641538672000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-019-00479-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4]]},"references-count":58,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["10.1007\/s00165-019-00479-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-019-00479-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4]]},"assertion":[{"value":"11 June 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 February 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}