{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:50Z","timestamp":1740099050365,"version":"3.37.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319893624"},{"type":"electronic","value":"9783319893631"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89363-1_17","type":"book-chapter","created":{"date-parts":[[2018,4,3]],"date-time":"2018-04-03T13:04:43Z","timestamp":1522760683000},"page":"301-318","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Abstract Family-Based Model Checking Using Modal Featured Transition Systems: Preservation of CTL$$^{\\star }$$\u22c6"],"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":[[2018,4,4]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37521-7","volume-title":"Feature-Oriented Software Product Lines - Concepts and Implementation","author":"S Apel","year":"2013","unstructured":"Apel, S., Batory, D.S., K\u00e4stner, C., Saake, G.: Feature-Oriented Software Product Lines - Concepts and Implementation. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37521-7"},{"key":"17_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge, London (2008)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"17_CR4","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":"17_CR5","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.: Model checking software product lines with SNIP. STTT 14(5), 589\u2013612 (2012). https:\/\/doi.org\/10.1007\/s10009-012-0234-1","journal-title":"STTT"},{"issue":"8","key":"17_CR6","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., Heymans, P., Legay, A., Raskin, J.: 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). http:\/\/doi.ieeecomputersociety.org\/10.1109\/TSE.2012.86","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_CR7","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). http:\/\/doi.acm.org\/10.1145\/1985793.1985838"},{"key":"17_CR8","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":"17_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44914-0_1","volume-title":"Abstraction, Reformulation, and Approximation","author":"P Cousot","year":"2000","unstructured":"Cousot, P.: Partial completeness of abstract fixpoint checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, pp. 1\u201325. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44914-0_1"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1016\/j.tcs.2014.01.016","volume":"560","author":"AS Dimovski","year":"2014","unstructured":"Dimovski, A.S.: Program verification using symbolic game semantics. Theor. Comput. Sci. 560, 364\u2013379 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.01.016","journal-title":"Theor. Comput. Sci."},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-32582-8_2","volume-title":"Model Checking Software","author":"AS Dimovski","year":"2016","unstructured":"Dimovski, A.S.: Symbolic game semantics for model checking program families. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 19\u201337. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-32582-8_2"},{"key":"17_CR12","unstructured":"Dimovski, A.S.: Abstract family-based model checking using modal featured transition systems: preservation of CTL$$^{\\star }$$\u22c6 (extended version). CoRR abs\/1802.04970 (2018). http:\/\/arxiv.org\/abs\/1802.04970"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.tcs.2017.09.029","volume":"706","author":"AS Dimovski","year":"2018","unstructured":"Dimovski, A.S.: Verifying annotated program families using symbolic game semantics. Theor. Comput. Sci. 706, 35\u201353 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2017.09.029","journal-title":"Theor. Comput. Sci."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-319-23404-5_18","volume-title":"Model Checking Software","author":"AS Dimovski","year":"2015","unstructured":"Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., W\u0105sowski, A.: Family-based model checking without a family-based model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282\u2013299. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_18"},{"issue":"5","key":"17_CR15","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). https:\/\/doi.org\/10.1007\/s10009-016-0425-2","journal-title":"STTT"},{"key":"17_CR16","doi-asserted-by":"publisher","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. 37, pp. 247\u2013270. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2015.247","DOI":"10.4230\/LIPIcs.ECOOP.2015.247"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-48989-6_14","volume-title":"FM 2016: Formal Methods","author":"AS Dimovski","year":"2016","unstructured":"Dimovski, A.S., Brabrand, C., W\u0105sowski, A.: Finding suitable variability abstractions for family-based analysis. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 217\u2013234. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_14"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-63121-9_13","volume-title":"Models, Algorithms, Logics and Tools","author":"AS Dimovski","year":"2017","unstructured":"Dimovski, A.S., W\u0105sowski, A.: From transition systems to variability models and from lifted model checking back to UPPAAL. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 249\u2013268. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_13"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-662-54494-5_24","volume-title":"Fundamental Approaches to Software Engineering","author":"AS Dimovski","year":"2017","unstructured":"Dimovski, A.S., W\u0105sowski, A.: Variability-specific abstraction refinement for family-based model checking. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 406\u2013423. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54494-5_24"},{"key":"17_CR20","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 2012, Beijing, China, 11\u201316 June 2012. pp. 323\u2013334. ACM (2012). http:\/\/doi.acm.org\/10.1145\/2254064.2254103"},{"key":"17_CR21","volume-title":"The SPIN Model Checker - Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"17_CR22","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1109\/ASE.2015.84","DOI":"10.1109\/ASE.2015.84"},{"issue":"1","key":"17_CR23","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). https:\/\/doi.org\/10.22152\/programming-journal.org\/2017\/1\/1","journal-title":"Program. J."},{"issue":"3","key":"17_CR24","doi-asserted-by":"crossref","first-page":"14:1","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:1\u201314:39 (2012). http:\/\/doi.acm.org\/10.1145\/2211616.2211617","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"17_CR25","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, pp. 805\u2013824 (2011). http:\/\/doi.acm.org\/10.1145\/2048066.2048128"},{"key":"17_CR26","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS 1988), pp. 203\u2013210. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/LICS.1988.5119","DOI":"10.1109\/LICS.1988.5119"},{"key":"17_CR27","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). https:\/\/doi.org\/10.1016\/j.scico.2015.04.005","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"17_CR28","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). https:\/\/doi.org\/10.1016\/S0167-6423(00)00018-6","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"17_CR29","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.jlamp.2015.06.007","volume":"85","author":"A Rhein von","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. Algebr. Methods Program. 85(1), 125\u2013145 (2016). https:\/\/doi.org\/10.1016\/j.jlamp.2015.06.007","journal-title":"J. Log. Algebr. Methods Program."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89363-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,17]],"date-time":"2022-08-17T22:25:34Z","timestamp":1660775134000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89363-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893624","9783319893631"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89363-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}