{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:00:59Z","timestamp":1770289259776,"version":"3.49.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2016,5,26]],"date-time":"2016-05-26T00:00:00Z","timestamp":1464220800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10009-016-0425-2","type":"journal-article","created":{"date-parts":[[2016,5,26]],"date-time":"2016-05-26T15:23:01Z","timestamp":1464276181000},"page":"585-603","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Efficient family-based model checking via variability abstractions"],"prefix":"10.1007","volume":"19","author":[{"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmad Salim","family":"Al-Sibahi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claus","family":"Brabrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,26]]},"reference":[{"key":"425_CR1","doi-asserted-by":"crossref","unstructured":"Apel, S., Batory, D.S., K\u00e4stner, C., Saake, G.: Feature-oriented software product lines\u2014concepts and implementation. Springer (2013)","DOI":"10.1007\/978-3-642-37521-7"},{"key":"425_CR2","doi-asserted-by":"crossref","unstructured":"Apel, S., Speidel, H., Wendler, P., von Rhein, A., Beyer, D.: Detection of feature interactions using feature-aware verification. In: 26th IEEE\/ACM international conference on automated software engineering (ASE 2011), pp. 372\u2013375 (2011)","DOI":"10.1109\/ASE.2011.6100075"},{"key":"425_CR3","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)"},{"key":"425_CR4","doi-asserted-by":"crossref","unstructured":"Belder, T., ter Beek, M.H., de\u00a0Vink, E.P.: Coherent branching feature bisimulation. In: Proceedings 6th workshop on formal methods and analysis in SPL engineering, FMSPLE 2015, EPTCS, vol. 182, pp.14\u201330 (2015)","DOI":"10.4204\/EPTCS.182.2"},{"key":"425_CR5","doi-asserted-by":"crossref","unstructured":"Bodden, E., Tol\u00eado, T., Ribeiro, M., Brabrand, C., Borba, P., Mezini, M.: Spl $${}^{\\text{lift}}$$ 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":"425_CR6","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-642-36964-3_3","volume":"10","author":"C Brabrand","year":"2013","unstructured":"Brabrand, C., Ribeiro, M., Tol\u00eado, T., Winther, J., Borba, P.: Intraprocedural dataflow analysis for software product lines. Trans. Aspect Oriented Soft. Dev. 10, 73\u2013108 (2013)","journal-title":"Trans. Aspect Oriented Soft. Dev."},{"key":"425_CR7","doi-asserted-by":"crossref","unstructured":"Chen, S., Erwig, M., Walkingshaw, E.: An error-tolerant type system for variational lambda calculus. In: ACM SIGPLAN international conference on functional programming, ICFP\u201912, pp. 29\u201340 (2012)","DOI":"10.1145\/2364527.2364535"},{"issue":"4","key":"425_CR8","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. STTT 2(4), 410\u2013425 (2000)","journal-title":"STTT"},{"issue":"5","key":"425_CR9","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"Edmund M Clarke","year":"1994","unstructured":"Clarke, Edmund M., Grumberg, Orna, Long, David E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"12","key":"425_CR10","doi-asserted-by":"crossref","first-page":"1130","DOI":"10.1016\/j.scico.2010.10.005","volume":"76","author":"A Classen","year":"2011","unstructured":"Classen, A., Boucher, Q., Heymans, P.: A text-based approach to feature modelling: syntax and semantics of TVL. Sci. Comput. Program. 76(12), 1130\u20131143 (2011)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"425_CR11","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/s10009-012-0234-1","volume":"14","author":"A Classen","year":"2012","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y.: model checking software product lines with SNIP. STTT 14(5), 589\u2013612 (2012)","journal-title":"STTT"},{"issue":"8","key":"425_CR12","doi-asserted-by":"crossref","first-page":"1069","DOI":"10.1109\/TSE.2012.86","volume":"39","author":"A Classen","year":"2013","unstructured":"Classen, A., Cordy, M., Schobbens, P.-Y., Heymans, P., Legay, A., Raskin, J.-F.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Software Eng. 39(8), 1069\u20131089 (2013)","journal-title":"IEEE Trans. Software Eng."},{"key":"425_CR13","doi-asserted-by":"crossref","unstructured":"Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd international conference on software engineering, ICSE 2011, pp. 321\u2013330 (2011)","DOI":"10.1145\/1985793.1985838"},{"key":"425_CR14","doi-asserted-by":"crossref","unstructured":"Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A., Raskin, J.-F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM\/IEEE international conference on software engineering\u2014Volume 1, ICSE 2010, pp. 335\u2013344 (2010)","DOI":"10.1145\/1806799.1806850"},{"key":"425_CR15","unstructured":"Clements, P., Northrop, L.: Software product lines: practices and patterns. Addison-Wesley (2001)"},{"key":"425_CR16","doi-asserted-by":"crossref","unstructured":"Cordy, M., Classen, A., Perrouin, G., Schobbens, P.-Y., Heymans, P., Legay, A.: Simulation-based abstractions for software product-line model checking. In: Proceedings of the 34th international conference on software engineering, ICSE 2012, pp. 672\u2013682 (2012)","DOI":"10.1109\/ICSE.2012.6227150"},{"key":"425_CR17","doi-asserted-by":"crossref","unstructured":"Cordy, M., Heymans, P., Legay, A., Schobbens, P.-Y., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of product-line behavioural models. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, (FSE-22), pp. 190\u2013201 (2014)","DOI":"10.1145\/2635868.2635919"},{"key":"425_CR18","unstructured":"Cousot, P,: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbr\u00fcggen, R. (eds.) Calculational system design. NATO ASI Series F. IOS Press, Amsterdam (1999)"},{"key":"425_CR19","doi-asserted-by":"crossref","unstructured":"Czarnecki, K., Antkiewicz, M.: Mapping features to models: a template approach based on superimposed variants. In: Generative programming and component engineering, 4th Int. Conf., GPCE 2005, LNCS, vol. 3676, pp. 422\u2013437 (2005)","DOI":"10.1007\/11561347_28"},{"issue":"2","key":"425_CR20","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253\u2013291 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"425_CR21","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1016\/j.tcs.2014.01.016","volume":"560","author":"Aleksandar S Dimovski","year":"2014","unstructured":"Dimovski, Aleksandar S.: Program verification using symbolic game semantics. Theor. Comput. Sci. 560, 364\u2013379 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"425_CR22","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S.: Symbolic game semantics for model checking program families. In: Model Checking Software\u201423nd International Symposium, SPIN 2016, Proceedings, LNCS, vol. 9641, pp. 19\u201337. Springer (2016)","DOI":"10.1007\/978-3-319-32582-8_2"},{"key":"425_CR23","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Family-based model checking without a family-based model checker. In: Model checking software\u201422nd International Symposium, SPIN 2015, Proceedings, LNCS, vol. 9232, pp. 282\u2013299. Springer (2015)","DOI":"10.1007\/978-3-319-23404-5_18"},{"key":"425_CR24","unstructured":"Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions: trading precision for speed in family-based analyses. In: 29th European conference on object-oriented programming, ECOOP 2015, LIPIcs, vol.\u00a037, pp. 247\u2013270. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)"},{"key":"425_CR25","unstructured":"Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions: trading precision for speed in family-based analyses (extended version). CoRR, abs\/1503.04608 (2015)"},{"key":"425_CR26","unstructured":"Fantechi, A., Gnesi, S.: A behavioural model for product families. In: Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007, pp. 521\u2013524. ACM (2007)"},{"issue":"2\u20133","key":"425_CR27","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/s10009-003-0122-9","volume":"5","author":"M Gallardo","year":"2004","unstructured":"Gallardo, M., Mart\u00ednez, J., Merino, P., Pimentel, E.: $$\\alpha $$ \u03b1 spin: a tool for abstract model checking. STTT 5(2\u20133), 165\u2013184 (2004)","journal-title":"STTT"},{"key":"425_CR28","doi-asserted-by":"crossref","unstructured":"Gallardo, M., Merino, P., Pimentel, E.: Refinement of LTL formulas for abstract model checking. In: Static analysis, 9th international symposium, SAS 2002, Proceedings, LNCS, vol. 2477, pp. 395\u2013410. Springer (2002)","DOI":"10.1007\/3-540-45789-5_28"},{"key":"425_CR29","doi-asserted-by":"crossref","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.D.: Modeling and model checking software product lines. In: Formal methods for open object-based distributed systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Proceedings, LNCS, vol. 5051, pp. 113\u2013131. Springer (2008)","DOI":"10.1007\/978-3-540-68863-1_8"},{"key":"425_CR30","unstructured":"Holzmann, G.J.: The SPIN Model Checker\u2014primer and reference manual. Addison-Wesley (2004)"},{"key":"425_CR31","doi-asserted-by":"crossref","unstructured":"Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E.,\u00a0Spencer Peterson, A.: Feature-oriented domain analysis (FODA) feasibility study. Technical report, Carnegie-Mellon University Software Engineering Institute (1990)","DOI":"10.21236\/ADA235785"},{"issue":"3","key":"425_CR32","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/2211616.2211617","volume":"21","author":"C K\u00e4stner","year":"2012","unstructured":"K\u00e4stner, C., Apel, S., Th\u00fcm, T., Saake, G.: Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21(3), 14 (2012)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"425_CR33","doi-asserted-by":"crossref","unstructured":"K\u00e4stner, C., Giarrusso, P.G., Rendel, T., Erdweg, S., Ostermann, K., Berger, T.: 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 (2011)","DOI":"10.1145\/2048066.2048128"},{"issue":"1","key":"425_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1049\/ip-d.1983.0001","volume":"130","author":"J Kramer","year":"1983","unstructured":"Kramer, J., Magee, J., Sloman, M., Lister, A.: Conic: An integrated approach to distributed computer control systems. IEE Proc. 130(1), 1\u201310 (1983)","journal-title":"IEE Proc."},{"key":"425_CR35","unstructured":"Lauenroth, K., Pohl, K., Toehning, S.: Model checking of domain artifacts in product line engineering. In: ASE 2009, 24th IEEE\/ACM International Conference on Automated Software Engineering, 2009, pp. 269\u2013280. IEEE Computer Society (2009)"},{"issue":"1","key":"425_CR36","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/j.jlamp.2015.09.004","volume":"85","author":"M Lochau","year":"2016","unstructured":"Lochau, M., Mennicke, S., Baller, H., Ribbeck, L.: Incremental model checking of delta-oriented software product lines. J. Log. Algebraic Methods Program. 85(1), 245\u2013267 (2016)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"425_CR37","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6(1), 11\u201344 (1995)","journal-title":"Formal Methods Syst. Des."},{"key":"425_CR38","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Applications of craig interpolants in model checking. In: Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Proceedings, LNCS, vol. 3440, pp. 1\u201312. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_1"},{"key":"425_CR39","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/j.scico.2015.04.005","volume":"105","author":"J Midtgaard","year":"2015","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)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"425_CR40","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/S0167-6423(00)00018-6","volume":"41","author":"M Plath","year":"2001","unstructured":"Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53\u201384 (2001)","journal-title":"Sci. Comput. Program."},{"key":"425_CR41","doi-asserted-by":"crossref","unstructured":"Post, H., Sinz, C.: Configuration lifting: verification meets software configuration. In: 23rd IEEE\/ACM international conference on automated software engineering (ASE 2008), pp. 347\u2013350 (2008)","DOI":"10.1109\/ASE.2008.45"},{"key":"425_CR42","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Using FMC for family-based analysis of software product lines. In: Proceedings of the 19th international conference on software product line, SPLC 2015, pp. 432\u2013439. ACM (2015)","DOI":"10.1145\/2791060.2791118"},{"issue":"2","key":"425_CR43","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/j.jlamp.2015.11.006","volume":"85","author":"MH Beek ter","year":"2016","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebraic Methods Program. 85(2), 287\u2013315 (2016)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"425_CR44","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1145\/2580950","volume":"47","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm, T., Apel, S., K\u00e4stner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6 (2014)","journal-title":"ACM Comput. Surv."},{"key":"425_CR45","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: Generative programming and component engineering, GPCE\u201912, pp. 11\u201320. ACM (2012)","DOI":"10.1145\/2371401.2371404"},{"key":"425_CR46","unstructured":"Th\u00fcm, T., Winkelmann, T., Schr\u00f6ter, R., Hentschel, M., Kr\u00fcger, S.: Variability hiding in contracts for dependent software product lines. In: Proceedings of the tenth international workshop on variability modelling of software-intensive systems, 2016, pp. 97\u2013104. ACM (2016)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0425-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0425-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0425-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0425-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T22:43:42Z","timestamp":1567982622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-016-0425-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5,26]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["425"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0425-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5,26]]}}}