{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:17:22Z","timestamp":1759637842718,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030167219"},{"type":"electronic","value":"9783030167226"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-16722-6_11","type":"book-chapter","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T02:01:08Z","timestamp":1554343268000},"page":"192-209","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Variability Abstraction and Refinement for Game-Based Lifted Model Checking of Full CTL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-2631","authenticated-orcid":false,"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0532-2685","authenticated-orcid":false,"given":"Andrzej","family":"Wasowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,4]]},"reference":[{"key":"11_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":"11_CR2","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.jlamp.2015.09.004","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. Algebr. Methods Program. 85(2), 287\u2013315 (2016). \n                      https:\/\/doi.org\/10.1016\/j.jlamp.2015.09.004","journal-title":"J. Log. Algebr. Methods Program."},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-04761-9_22","volume-title":"Automated Technology for Verification and Analysis","author":"A Campetelli","year":"2009","unstructured":"Campetelli, A., Gruler, A., Leucker, M., Thoma, D.: Don\u2019t Know for multi-valued systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 289\u2013305. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-04761-9_22"},{"issue":"8","key":"11_CR4","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). \n                      http:\/\/doi.ieeecomputersociety.org\/10.1109\/TSE.2012.86","journal-title":"IEEE Trans. Softw. Eng."},{"key":"11_CR5","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). \n                      http:\/\/doi.acm.org\/10.1145\/1985793.1985838"},{"key":"11_CR6","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":"11_CR7","unstructured":"Cordy, M., Classen, A., Heymans, P., Schobbens, P., Legay, A.: Provelines: a product line of verifiers for software product lines. In: 17th International SPLC 2013 Workshops, pp. 141\u2013146. ACM (2013). \n                      http:\/\/doi.acm.org\/10.1145\/2499777.2499781"},{"key":"11_CR8","unstructured":"Cordy, M., Heymans, P., Legay, A., Schobbens, P., 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. ACM (2014). \n                      http:\/\/doi.acm.org\/10.1145\/2635868.2635919"},{"key":"11_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). \n                      https:\/\/doi.org\/10.1007\/3-540-44914-0_1"},{"key":"11_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). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2014.01.016","journal-title":"Theor. Comput. Sci."},{"key":"11_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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-32582-8_2"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-319-89363-1_17","volume-title":"Fundamental Approaches to Software Engineering","author":"AS Dimovski","year":"2018","unstructured":"Dimovski, A.S.: Abstract family-based model checking using modal featured transition systems: preservation of CTL\n                      \n                        \n                      \n                      $$^{\\star }$$\n                    . In: Russo, A., Sch\u00fcrr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 301\u2013318. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-89363-1_17"},{"key":"11_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). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2017.09.029","journal-title":"Theor. Comput. Sci."},{"key":"11_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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-23404-5_18"},{"issue":"5","key":"11_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). \n                      https:\/\/doi.org\/10.1007\/s10009-016-0425-2","journal-title":"STTT"},{"key":"11_CR16","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 (extended version). CoRR (2019). \n                      http:\/\/arxiv.org\/","DOI":"10.1007\/978-3-030-16722-6_11"},{"key":"11_CR17","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63121-9_13"},{"key":"11_CR18","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). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54494-5_24"},{"issue":"8","key":"11_CR19","doi-asserted-by":"publisher","first-page":"1130","DOI":"10.1016\/j.ic.2006.10.009","volume":"205","author":"O Grumberg","year":"2007","unstructured":"Grumberg, O., Lange, M., Leucker, M., Shoham, S.: When not losing is better than winning: abstraction and refinement for the full mu-calculus. Inf. Comput. 205(8), 1130\u20131148 (2007). \n                      https:\/\/doi.org\/10.1016\/j.ic.2006.10.009","journal-title":"Inf. Comput."},{"issue":"1","key":"11_CR20","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). \n                      https:\/\/doi.org\/10.22152\/programming-journal.org\/2017\/1\/1","journal-title":"Program. J."},{"key":"11_CR21","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: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64\u201379. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-71316-6_6"},{"key":"11_CR22","doi-asserted-by":"crossref","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). \n                      http:\/\/dx.doi.org\/10.1109\/LICS.1988.5119","DOI":"10.1109\/LICS.1988.5119"},{"issue":"1","key":"11_CR23","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). \n                      https:\/\/doi.org\/10.1016\/S0167-6423(00)00018-6","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"11_CR24","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). \n                      https:\/\/doi.org\/10.1145\/1297658.1297659","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"11_CR25","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). \n                      https:\/\/doi.org\/10.1016\/j.ic.2009.10.002","journal-title":"Inf. Comput."},{"key":"11_CR26","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3550-5","volume-title":"Modal and Temporal Properties of Processes","author":"C Stirling","year":"2001","unstructured":"Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, New York (2001). \n                      https:\/\/doi.org\/10.1007\/978-1-4757-3550-5"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-16722-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:07:00Z","timestamp":1558343220000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-16722-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030167219","9783030167226"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-16722-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"4 April 2019","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"74","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}