{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:04:52Z","timestamp":1767236692263},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T00:00:00Z","timestamp":1565308800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T00:00:00Z","timestamp":1565308800000},"content-version":"vor","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":[[2020,2]]},"DOI":"10.1007\/s10009-019-00528-0","type":"journal-article","created":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T16:03:30Z","timestamp":1565366610000},"page":"35-55","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["$$\\hbox {CTL}^{\\star }$$ family-based model checking using variability abstractions and modal transition systems"],"prefix":"10.1007","volume":"22","author":[{"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,9]]},"reference":[{"key":"528_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7","volume-title":"Feature-Oriented Software Product Lines\u2014Concepts and Implementation","author":"S Apel","year":"2013","unstructured":"Apel, S., Batory, D.S., K\u00e4stner, C., Saake, G.: Feature-Oriented Software Product Lines\u2014Concepts and Implementation. Springer, Berlin (2013)"},{"key":"528_CR2","doi-asserted-by":"crossref","unstructured":"Apel, S., Rhein, A., von Wendler, P., Gr\u00f6\u00dflinger, A., Beyer, D.: Strategies for product-line verification: case studies and experiments. In: 35th International Conference on Software Engineering, ICSE \u201913, pp. 482\u2013491. IEEE Computer Society (2013)","DOI":"10.1109\/ICSE.2013.6606594"},{"key":"528_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"528_CR4","doi-asserted-by":"crossref","unstructured":"Ben-David, S., Sterin, B., Atlee, J.M., Beidu, S.: Symbolic model checking of product-line requirements using sat-based methods. In: 37th IEEE\/ACM International Conference on Software Engineering, ICSE 2015, Volume 1, pp. 189\u2013199. IEEE Computer Society (2015)","DOI":"10.1109\/ICSE.2015.40"},{"key":"528_CR5","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":"528_CR6","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"Alessandro Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. In: Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings, volume 2404 of LNCS, pp. 359\u2013364. Springer (2002)"},{"key":"528_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, Workshop, 1981, volume 131 of Lecture Notes in Computer Science, pp. 52\u201371. Springer (1981)","DOI":"10.1007\/BFb0025774"},{"key":"528_CR8","doi-asserted-by":"crossref","unstructured":"Classen, A.: CTL model checking for software product lines in NuSMV. Technical Report, P-CS-TR SPLMC-00000002, University Of Namur, pp. 1\u201317 (2011)","DOI":"10.1145\/1985793.1985838"},{"issue":"5","key":"528_CR9","doi-asserted-by":"publisher","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":"528_CR10","doi-asserted-by":"publisher","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. Softw. Eng. 39(8), 1069\u20131089 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"528_CR11","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. ACM (2011)","DOI":"10.1145\/1985793.1985838"},{"key":"528_CR12","volume-title":"Software Product Lines: Practices and Patterns","author":"P Clements","year":"2001","unstructured":"Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley, Boston (2001)"},{"key":"528_CR13","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: Glinz, M., Murphy, G.C., Pezz\u00e8, M. (eds.) 34th International Conference on Software Engineering, ICSE 2012, pp. 672\u2013682. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227150"},{"key":"528_CR14","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: Cheung, S.-C. Orso, A., Storey, M.-A.D. (eds.) Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), pp. 190\u2013201. ACM (2014)","DOI":"10.1145\/2635868.2635919"},{"key":"528_CR15","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Partial completeness of abstract fixpoint checking. In: Abstraction, Reformulation, and Approximation, 4th International Symposium, SARA 2000, Proceedings, volume 1864 of LNCS, pp. 1\u201325. Springer (2000)","DOI":"10.1007\/3-540-44914-0_1"},{"key":"528_CR16","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-319-89363-1_17","volume-title":"Fundamental Approaches to Software Engineering","author":"Aleksandar S. Dimovski","year":"2018","unstructured":"Dimovski, A.S.: Abstract family-based model checking using modal featured transition systems: Preservation of ctl$$^{\\star }$$. In: Fundamental Approaches to Software Engineering\u201421st International Conference, FASE 2018, Proceedings, volume 10802 of LNCS, pp. 301\u2013318. Springer (2018)"},{"key":"528_CR17","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-319-23404-5_18","volume-title":"Model Checking Software","author":"Aleksandar S. Dimovski","year":"2015","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, volume 9232 of LNCS, pp. 282\u2013299. Springer (2015)"},{"issue":"5","key":"528_CR18","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10009-016-0425-2","volume":"19","author":"AS Dimovski","year":"2017","unstructured":"Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Efficient family-based model checking via variability abstractions. STTT 19(5), 585\u2013603 (2017)","journal-title":"STTT"},{"key":"528_CR19","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, volume\u00a037 of LIPIcs, pp. 247\u2013270. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik (2015)"},{"key":"528_CR20","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-48989-6_14","volume-title":"FM 2016: Formal Methods","author":"Aleksandar S. Dimovski","year":"2016","unstructured":"Dimovski, A.S., Brabrand, C., Wasowski, A.: Finding suitable variability abstractions for family-based analysis. In: FM 2016: Formal Methods\u201421st International Symposium, Proceedings, volume 9995 of LNCS, pp. 217\u2013234 (2016)"},{"key":"528_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2017.12.012","volume":"159","author":"AS Dimovski","year":"2018","unstructured":"Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions for lifted analyses. Sci. Comput. Program. 159, 1\u201327 (2018)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"528_CR22","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s00165-019-00479-y","volume":"31","author":"AS Dimovski","year":"2019","unstructured":"Dimovski, A.S., Brabrand, C., Wasowski, A.: Finding suitable variability abstractions for lifted analysis. Formal Asp. Comput. 31(2), 231\u2013259 (2019)","journal-title":"Formal Asp. Comput."},{"key":"528_CR23","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S., Legay, A., Wasowski, A.: Variability abstraction and refinement for game-based lifted model checking of full CTL. In: Fundamental Approaches to Software Engineering\u201422nd International Conference, FASE 2019, Proceedings, volume 11424 of LNCS, pp. 192\u2013209. Springer (2019)","DOI":"10.1007\/978-3-030-16722-6_11"},{"key":"528_CR24","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S., Wasowski, A.: 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, pp. 249\u2013268. Springer (2017)","DOI":"10.1007\/978-3-319-63121-9_13"},{"key":"528_CR25","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S., Wasowski, A.: 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 (2017)","DOI":"10.1007\/978-3-662-54494-5_24"},{"issue":"4","key":"528_CR26","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/MC.2009.118","volume":"42","author":"C Ebert","year":"2009","unstructured":"Ebert, C., Jones, C.: Embedded software: facts, figures, and future. IEEE Comput. 42(4), 42\u201352 (2009)","journal-title":"IEEE Comput."},{"key":"528_CR27","unstructured":"Gazzillo, P., Grimm, R.: 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 \u201912, Beijing, China\u2014June 11\u201316, 2012, pp. 323\u2013334. ACM (2012)"},{"key":"528_CR28","first-page":"113","volume-title":"Lecture Notes in Computer Science","author":"Alexander Gruler","year":"2008","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, volume 5051 of LNCS, pp. 113\u2013131. Springer (2008)"},{"key":"528_CR29","doi-asserted-by":"crossref","unstructured":"Iosif-Lazar, A.F., Al-Sibahi, A.S., Dimovski, A.S., Savolainen, J.E., Sierszecki, K., Wasowski, A.: 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 (2015)","DOI":"10.1109\/ASE.2015.84"},{"issue":"1","key":"528_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.22152\/programming-journal.org\/2017\/1\/1","volume":"1","author":"AF Iosif-Lazar","year":"2017","unstructured":"Iosif-Lazar, A.F., Melo, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Effective analysis of c programs by rewriting variability. Program. J. 1(1), 1 (2017)","journal-title":"Program. J."},{"issue":"3","key":"528_CR31","doi-asserted-by":"publisher","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."},{"issue":"10","key":"528_CR32","doi-asserted-by":"publisher","first-page":"805","DOI":"10.1145\/2076021.2048128","volume":"46","author":"Christian K\u00e4stner","year":"2011","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 Conf. on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011. pp. 805\u2013824 (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"528_CR33","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"528_CR34","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-71316-6_6","volume-title":"Programming Languages and Systems","author":"Kim G. Larsen","year":"2007","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: 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, pp. 64\u201379. Springer (2007)"},{"key":"528_CR35","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS \u201988), pp. 203\u2013210. IEEE Computer Society (1988)"},{"issue":"1","key":"528_CR36","doi-asserted-by":"publisher","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."},{"key":"528_CR37","doi-asserted-by":"publisher","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":"528_CR38","doi-asserted-by":"publisher","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."},{"issue":"1","key":"528_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1297658.1297659","volume":"9","author":"S Shoham","year":"2007","unstructured":"Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Log. 9(1), 1 (2007)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"528_CR40","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1016\/j.ic.2009.10.002","volume":"208","author":"S Shoham","year":"2010","unstructured":"Shoham, S., Grumberg, O.: Compositional verification and 3-valued abstractions join forces. Inf. Comput. 208(2), 178\u2013202 (2010)","journal-title":"Inf. Comput."},{"key":"528_CR41","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de\u00a0Vink, E.P., Willemse, T.A.C.: Family-based model checking with mcrl2. In: Fundamental Approaches to Software Engineering\u201420th International Conference, FASE 2017, Proceedings, volume 10202 of LNCS, pp. 387\u2013405 (2017)","DOI":"10.1007\/978-3-662-54494-5_23"},{"issue":"2","key":"528_CR42","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.jlamp.2015.11.006","volume":"85","author":"MH ter Beek","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":"528_CR43","doi-asserted-by":"publisher","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."},{"issue":"1","key":"528_CR44","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.jlamp.2015.06.007","volume":"85","author":"A von Rhein","year":"2016","unstructured":"von Rhein, A., Th\u00fcm, T., Schaefer, I., Liebig, J., Apel, S.: Variability encoding: from compile-time to load-time variability. J. Log. Algebraic Methods Program. 85(1), 125\u2013145 (2016)","journal-title":"J. Log. Algebraic Methods Program."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00528-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00528-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00528-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,25]],"date-time":"2022-09-25T11:56:19Z","timestamp":1664106979000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00528-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,9]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,2]]}},"alternative-id":["528"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00528-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,8,9]]},"assertion":[{"value":"9 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}