{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:04:42Z","timestamp":1762459482222,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662544938"},{"type":"electronic","value":"9783662544945"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54494-5_24","type":"book-chapter","created":{"date-parts":[[2017,3,22]],"date-time":"2017-03-22T00:09:02Z","timestamp":1490141342000},"page":"406-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Variability-Specific Abstraction Refinement for Family-Based Model Checking"],"prefix":"10.1007","author":[{"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[]},{"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,22]]},"reference":[{"key":"24_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"2","key":"24_CR2","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. Algebr. Meth. Program. 85(2), 287\u2013315 (2016). http:\/\/dx.doi.org\/10.1016\/j.jlamp.2015.09.004","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"24_CR3","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 2013, pp. 355\u2013364 (2013)","DOI":"10.1145\/2499370.2491976"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi:10.1007\/10722167_15"},{"issue":"2\u20133","key":"24_CR5","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"EM Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Meth. Syst. Des. 25(2\u20133), 105\u2013127 (2004). http:\/\/dx.doi.org\/10.1023\/B:FORM.0000040025.89719.f3","journal-title":"Formal Meth. Syst. Des."},{"issue":"12","key":"24_CR6","doi-asserted-by":"publisher","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). http:\/\/dx.doi.org\/10.1016\/j.scico.2010.10.005","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"24_CR7","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). http:\/\/dx.doi.org\/10.1007\/s10009-012-0234-1","journal-title":"STTT"},{"issue":"8","key":"24_CR8","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., 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":"24_CR9","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, Reading (2001)"},{"key":"24_CR10","unstructured":"Cordy, M., Heymans, P., Legay, A., Schobbens, P., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of product-line behavioural models. In: Cheung, S., Orso, A., Storey, M.D. (eds.) Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE-22), pp. 190\u2013201. ACM (2014). http:\/\/doi.acm.org\/10.1145\/2635868.2635919"},{"key":"24_CR11","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). http:\/\/dx.doi.org\/10.1016\/j.tcs.2014.01.016","journal-title":"Theor. Comput. Sci."},{"key":"24_CR12","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, Heidelberg (2016). doi:10.1007\/978-3-319-32582-8_2"},{"key":"24_CR13","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, Heidelberg (2015). doi:10.1007\/978-3-319-23404-5_18"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Efficient family-based model checking via variability abstractions. STTT 1\u201319 (2016). doi:10.1007\/s10009-016-0425-2","DOI":"10.1007\/s10009-016-0425-2"},{"key":"24_CR15","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). http:\/\/dx.doi.org\/10.4230\/LIPIcs.ECOOP.2015.247"},{"key":"24_CR16","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, Heidelberg (2016). doi:10.1007\/978-3-319-48989-6_14"},{"key":"24_CR17","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":"24_CR18","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, pp. 232\u2013244. ACM (2004). http:\/\/doi.acm.org\/10.1145\/964001.964021"},{"key":"24_CR19","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, Reading (2004)"},{"key":"24_CR20","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). http:\/\/dx.doi.org\/10.1109\/ASE.2015.84","DOI":"10.1109\/ASE.2015.84"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Iosif-Lazar, A.F., Melo, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Effective analysis of c programs by rewriting variability. In: The Art, Science, and Engineering of Programming, Programming 2017 (2017)","DOI":"10.22152\/programming-journal.org\/2017\/1\/1"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-oriented domain analysis (FODA) feasibility study. Technical report, Carnegie-Mellon University Software Engineering Institute, November 1990","DOI":"10.21236\/ADA235785"},{"issue":"3","key":"24_CR23","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."},{"key":"24_CR24","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"},{"issue":"1","key":"24_CR25","doi-asserted-by":"publisher","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":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-71316-6_6","volume-title":"Programming Languages and Systems","author":"KG Larsen","year":"2007","unstructured":"Larsen, K.G., Nyman, U., W\u0105sowski, A.: Modal I\/O automata for interface and product line theories. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64\u201379. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-71316-6_6"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1\u201312. Springer, Heidelberg (2005). doi:10.1007\/978-3-540-31980-1_1"},{"key":"24_CR28","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). http:\/\/dx.doi.org\/10.1016\/j.scico.2015.04.005","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"24_CR29","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. Algebr. Meth. Program. 85(1), 125\u2013145 (2016). http:\/\/dx.doi.org\/10.1016\/j.jlamp.2015.06.007","journal-title":"J. Log. Algebr. Meth. Program."},{"issue":"1","key":"24_CR30","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). http:\/\/doi.acm.org\/10.1145\/2580950","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54494-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:25:26Z","timestamp":1618971926000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54494-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544938","9783662544945"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54494-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"22 March 2017","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":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}