{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T16:57:42Z","timestamp":1772038662183,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2012,6,14]],"date-time":"2012-06-14T00:00:00Z","timestamp":1339632000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,10]]},"DOI":"10.1007\/s10009-012-0234-1","type":"journal-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T01:33:03Z","timestamp":1341797583000},"page":"589-612","source":"Crossref","is-referenced-by-count":91,"title":["Model checking software product lines with SNIP"],"prefix":"10.1007","volume":"14","author":[{"given":"Andreas","family":"Classen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maxime","family":"Cordy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Heymans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Yves","family":"Schobbens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,14]]},"reference":[{"key":"234_CR1","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: ASE 2011, pp. 372\u2013375. IEEE (2011)","DOI":"10.1109\/ASE.2011.6100075"},{"key":"234_CR2","doi-asserted-by":"crossref","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A logical framework to deal with variability. In: IFM \u201910. LNCS, vol. 6396, pp. 43\u201358. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16265-7_5"},{"key":"234_CR3","doi-asserted-by":"crossref","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: Formal description of variability in product families. In: SPLC\u201911, pp. 130\u2013139. IEEE CS (2011)","DOI":"10.1145\/1985484.1985492"},{"key":"234_CR4","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2007","unstructured":"Baier C., Katoen J.-P.: Principles of Model Checking. MIT Press, Boca Raton (2007)"},{"key":"234_CR5","doi-asserted-by":"crossref","unstructured":"Batory, D.S.: Feature models, grammars, and propositional formulas. In: SPLC \u201905. LNCS, vol. 3714, pp. 7\u201320. Springer, Berlin (2005)","DOI":"10.1007\/11554844_3"},{"key":"234_CR6","doi-asserted-by":"crossref","unstructured":"Boucher, Q., Classen, A., Heymans, P., Bourdoux, A., Demonceau, L.: Tag and prune: a pragmatic approach to software product line implementation. In: ASE \u201910, pp. 333\u2013336. ACM, New York (2010)","DOI":"10.1145\/1858996.1859064"},{"issue":"3","key":"234_CR7","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"key":"234_CR8","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti A., Clarke E., Giunchiglia F., Roveri M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2, 410\u2013425 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"234_CR9","unstructured":"Classen, A. http:\/\/www.info.fundp.ac.be\/~acs\/fts . (2010)"},{"key":"234_CR10","unstructured":"Classen, A.: Modelling and Model Checking Variability-Intensive Systems. PhD thesis, PReCISE Research Centre, Faculty of Computer Science, University of Namur (FUNDP), 5000 Namur, Belgium (2011)"},{"key":"234_CR11","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. Programm. 76, 1130\u20131143 (2011)","journal-title":"Sci. Comput. Programm."},{"key":"234_CR12","doi-asserted-by":"crossref","unstructured":"Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: Symbolic model checking of software product lines. In: ICSE \u201911, pp. 321\u2013330. ACM, New York (2011)","DOI":"10.1145\/1985793.1985838"},{"key":"234_CR13","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: ICSE \u201910, pp. 335\u2013344. ACM, New York (2010)","DOI":"10.1145\/1806799.1806850"},{"key":"234_CR14","unstructured":"Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A., Raskin, J.-F.: Modelling and model checking variability-intensive systems with featured transition systems. IEEE Trans. Softw. Eng. (2012) (Submitted)"},{"key":"234_CR15","unstructured":"Consultative Committee for Space Data Systems (CCSDS). CCSDS File Delivery Protocol (CFDP): Blue Book, Issue 4. Number CCSDS 727.0-B-4. NASA (2007)"},{"key":"234_CR16","doi-asserted-by":"crossref","unstructured":"Czarnecki, K., Antkiewicz, M.: Mapping features to models: a template approach based on superimposed variants. In: Gluck, R., Lowry, M. (eds.) GPCE \u201905. LNCS, vol. 3676, pp. 422\u2013437. Springer, Berlin (2005)","DOI":"10.1007\/11561347_28"},{"key":"234_CR17","doi-asserted-by":"crossref","unstructured":"Fantechi, A., Gnesi, S.: Formal modeling for product families engineering. In: SPLC \u201908, pp. 193\u2013202. IEEE (2008)","DOI":"10.1109\/SPLC.2008.45"},{"key":"234_CR18","doi-asserted-by":"crossref","unstructured":"Fischbein, D., Uchitel, S., Braberman, V.: A foundation for behavioural conformance in software product line architectures. In ROSATEA \u201906, ISSTA \u201906 workshop, pp. 39\u201348. ACM, New York (2006)","DOI":"10.1145\/1147249.1147254"},{"key":"234_CR19","doi-asserted-by":"crossref","unstructured":"Garrido, A., Johnson, R.: Analyzing multiple configurations of a C program. In: ICSM \u201905, pp. 379\u2013388. IEEE (2005)","DOI":"10.1109\/ICSM.2005.23"},{"key":"234_CR20","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to Bnchi automata translation. In: CAV \u201901. LNCS, vol. 2102, pp. 53\u201365. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"234_CR21","doi-asserted-by":"crossref","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: FMOODS \u201908. LNCS, vol. 5051, pp. 113\u2013131. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-68863-1_8"},{"key":"234_CR22","unstructured":"Holzmann, G.J.: State compression in SPIN. In: the 3rd SPIN Workshop (1997)"},{"key":"234_CR23","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Menlo Park (2004)"},{"issue":"4","key":"234_CR24","doi-asserted-by":"crossref","first-page":"21:1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R. Jhala","year":"2009","unstructured":"Jhala R., Majumdar R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009)","journal-title":"ACM Comput. Surv."},{"key":"234_CR25","doi-asserted-by":"crossref","unstructured":"Kang, K., Cohen, S., Hess, J., Novak, W., Peterson, S.: Feature-oriented domain analysis (FODA) feasibility study. Technical Report CMU\/SEI-90-TR-21, SEI (1990)","DOI":"10.21236\/ADA235785"},{"key":"234_CR26","doi-asserted-by":"crossref","unstructured":"K\u00e4stner, C., Apel, S., Kuhlemann, M.: Granularity in software product lines. In: ICSE \u201908, pp. 311\u2013320. ACM, New York (2008)","DOI":"10.1145\/1368088.1368131"},{"key":"234_CR27","doi-asserted-by":"crossref","unstructured":"K\u00e4stner, C., Giarrusso, P.G., Ostermann, K.: Partial preprocessing C code for variability analysis. In: VaMoS \u201911, ICPS, pp. 127\u2013136. ACM, New York (2011)","DOI":"10.1145\/1944892.1944908"},{"issue":"12","key":"234_CR28","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/1183236.1183270","volume":"49","author":"T. Kishi","year":"2006","unstructured":"Kishi T., Noda N.: Formal verification and software product lines. Commun. ACM 49(12), 73\u201377 (2006)","journal-title":"Commun. ACM"},{"issue":"1","key":"234_CR29","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1049\/ip-e.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. IEEE Proc. Comput. Digit. Tech. 130(1), 1\u201310 (1983)","journal-title":"IEEE Proc. Comput. Digit. Tech."},{"key":"234_CR30","doi-asserted-by":"crossref","unstructured":"Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 232\u2013246. Springer, Berlin (1989)","DOI":"10.1007\/3-540-52148-8_19"},{"key":"234_CR31","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Nyman, U., Wasowski, A.: Modal I\/O automata for interface and product line theories. In: ESOP \u201907. LNCS, vol. 4021, pp. 64\u201379. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"234_CR32","doi-asserted-by":"crossref","unstructured":"Lauenroth, K., T\u00f6hning, S., Pohl, K.: Model checking of domain artifacts in product line engineering. In: ASE \u201909, pp. 269\u2013280. IEEE\/ACM (2009)","DOI":"10.1109\/ASE.2009.16"},{"issue":"11","key":"234_CR33","doi-asserted-by":"crossref","first-page":"1879","DOI":"10.1016\/j.jss.2007.01.047","volume":"80","author":"J. Liu","year":"2007","unstructured":"Liu J., Dehlinger J., Lutz R.: Safety analysis of software product lines using state-based modeling. J. Syst. Softw. 80(11), 1879\u20131892 (2007)","journal-title":"J. Syst. Softw."},{"issue":"1","key":"234_CR34","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":"234_CR35","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS \u201997, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"234_CR36","doi-asserted-by":"crossref","unstructured":"Post, H., Sinz, C.: Configuration lifting: Verification meets software configuration. In: ASE\u201908, pp. 347\u2013350. IEEE CS (2008)","DOI":"10.1109\/ASE.2008.45"},{"key":"234_CR37","doi-asserted-by":"crossref","unstructured":"Schobbens, P.-Y., Heymans, P., Trigaux, J.-C., Bontemps, Y.: Feature Diagrams: A Survey and A Formal Semantics. In: RE \u201906, pp. 139\u2013148. IEEE CS (2006)","DOI":"10.1109\/RE.2006.23"},{"key":"234_CR38","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS \u201986, pp. 332\u2013344. IEEE (1986)"},{"key":"234_CR39","doi-asserted-by":"crossref","unstructured":"Ziadi, T., H\u00e9lou\u00ebt, L., J\u00e9z\u00e9quel, J.-M.: Towards a UML profile for software product lines. In: van der Linden, F. (ed.) PFE \u201903. LNCS, vol. 3014, pp. 129\u2013139. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-24667-1_10"}],"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-012-0234-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0234-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0234-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,20]],"date-time":"2022-01-20T16:54:58Z","timestamp":1642697698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0234-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,14]]},"references-count":39,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["234"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0234-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,14]]}}}