{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T10:04:22Z","timestamp":1760609062654},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,2,7]],"date-time":"2018-02-07T00:00:00Z","timestamp":1517961600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2018,4]]},"DOI":"10.1007\/s11704-016-6048-7","type":"journal-article","created":{"date-parts":[[2018,3,2]],"date-time":"2018-03-02T15:07:56Z","timestamp":1520003276000},"page":"264-279","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Efficient software product-line model checking using induction and a SAT solver"],"prefix":"10.1007","volume":"12","author":[{"given":"Fei","family":"He","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Gao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liangze","family":"Yin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,2,7]]},"reference":[{"key":"6048_CR1","volume-title":"Software Product Lines: Practices and Patterns","author":"P Clements","year":"2002","unstructured":"Clements P, Northrop L. Software Product Lines: Practices and Patterns. Boston, MA: Addison-Wesley, 2002"},{"key":"6048_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering","author":"K Pohl","year":"2005","unstructured":"Pohl K, B\u00f6ckle G, Van Der Linden F. Software Product Line Engineering. Berlin: Springer, 2005"},{"issue":"1","key":"6048_CR3","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 Computing Surveys, 2014, 47(1): 6","journal-title":"ACM Computing Surveys"},{"issue":"3","key":"6048_CR4","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1109\/TSE.2013.56","volume":"40","author":"M Galster","year":"2014","unstructured":"Galster M, Weyns D, Tofan D, Michalik B, Avgeriou P. Variability in software systems \u2014 a systematic literature review. IEEE Transactions on Software Engineering, 2014, 40(3): 282\u2013306","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6048_CR5","first-page":"265","volume-title":"Proceedings of the 13th International Software Product Line Conference","author":"F Dordowsky","year":"2009","unstructured":"Dordowsky F, Hipp W. Adopting software product line principles to manage software variants in a complex avionics system. In: Proceedings of the 13th International Software Product Line Conference. 2009, 265\u2013274"},{"key":"6048_CR6","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-15651-9_29","volume-title":"Proceedings of the 29th International Conference on Computer Safety, Reliability, and Security","author":"S Hutchesson","year":"2010","unstructured":"Hutchesson S, McDermid J. Development of high-integrity software product lines using model transformation. In: Proceedings of the 29th International Conference on Computer Safety, Reliability, and Security. 2010, 389\u2013401"},{"key":"6048_CR7","first-page":"2","volume-title":"Proceedings of International Workshop on Model-Based Methodologies for Pervasive and Embedded Software","author":"A Polzer","year":"2009","unstructured":"Polzer A, Kowalewski S, Botterweck G. Applying software product line techniques in model-based embedded systems engineering. In: Proceedings of International Workshop on Model-Based Methodologies for Pervasive and Embedded Software. 2009, 2\u201310"},{"key":"6048_CR8","first-page":"255","volume-title":"Proceedings of the 24th International Conference on Software Engineering","author":"R Ommering Van","year":"2002","unstructured":"Van Ommering R. Building product populations with software components. In: Proceedings of the 24th International Conference on Software Engineering. 2002, 255\u2013265"},{"key":"6048_CR9","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/978-3-642-33678-2_30","volume-title":"Proceedings of the 31st International Conference on Computer Safety, Reliability, and Security","author":"R T V Braga","year":"2012","unstructured":"Braga R T V, Junior O T, Branco K R C, Neris L D O, Lee J. Adapting a software product line engineering process for certifying safety critical embedded systems. In: Proceedings of the 31st International Conference on Computer Safety, Reliability, and Security. 2012, 352\u2013363"},{"key":"6048_CR10","volume-title":"Model Checking","author":"E M Clarke","year":"1999","unstructured":"Clarke E M, Grumberg O, Peled D. Model Checking. Cambridge: MIT press, 1999"},{"key":"6048_CR11","first-page":"335","volume-title":"Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering","author":"A Classen","year":"2010","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: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering. 2010, 335\u2013344"},{"key":"6048_CR12","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1145\/1985793.1985838","volume-title":"Proceedings of the 33rd International Conference on Software Engineering","author":"A Classen","year":"2011","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. 2011, 321\u2013330"},{"key":"6048_CR13","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-68863-1_8","volume-title":"Proceedings of the International Conference on Formal Methods for Open Object-Based Distributed Systems","author":"A Gruler","year":"2008","unstructured":"Gruler A, Leucker M, Scheidemann K. Modeling and model checking software product lines. In: Proceedings of the International Conference on Formal Methods for Open Object-Based Distributed Systems. 2008, 113\u2013131"},{"key":"6048_CR14","first-page":"269","volume-title":"Proceedings of the 24th IEEE\/ACM International Conference on Automated Software Engineering","author":"K Lauenroth","year":"2009","unstructured":"Lauenroth K, Pohl K, Toehning S. Model checking of domain artifacts in product line engineering. In: Proceedings of the 24th IEEE\/ACM International Conference on Automated Software Engineering. 2009, 269\u2013280"},{"key":"6048_CR15","first-page":"450","volume-title":"Giannakopoulou D, M\u00e9ry D, eds. FM 2012: Formal Methods. Berlin: Springer-Verlag","author":"M H T Beek","year":"2012","unstructured":"Beek M H T, Mazzanti F, Sulova A. VMC: a tool for product variability analysis. In: Giannakopoulou D, M\u00e9ry D, eds. FM 2012: Formal Methods. Berlin: Springer-Verlag, 2012, 450\u2013454"},{"key":"6048_CR16","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-29320-7_24","volume-title":"Proceedings of the International Conference on Fundamentals of Software Engineering","author":"H Sabouri","year":"2012","unstructured":"Sabouri H, Khosravi R. Efficient verification of evolving software product lines. In: Proceedings of the International Conference on Fundamentals of Software Engineering. 2012, 351\u2013358"},{"key":"6048_CR17","first-page":"472","volume-title":"Proceedings of the International Conference on Software Engineering","author":"M Cordy","year":"2013","unstructured":"Cordy M, Schobbens P Y, Heymans P, Legay A. Beyond boolean product-line model checking: dealing with feature attributes and multifeatures. In: Proceedings of the International Conference on Software Engineering. 2013, 472\u2013481"},{"key":"6048_CR18","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1145\/2499777.2499781","volume-title":"Proceedings of the 17th International Software Product Line Conference co-located workshops","author":"M Cordy","year":"2013","unstructured":"Cordy M, Classen A, Heymans P, Schobbens P Y, Legay A. ProVe-Lines: a product line of verifiers for software product lines. In: Proceedings of the 17th International Software Product Line Conference co-located workshops. 2013, 141\u2013146"},{"key":"6048_CR19","volume-title":"Proceedings of the 6th Workshop on Programming Languages and Operating Systems","author":"R Tartler","year":"2011","unstructured":"Tartler R, Lohmann D, Dietrich C, Egger C, Sincero J. Configuration coverage in the analysis of large-scale system software. In: Proceedings of the 6th Workshop on Programming Languages and Operating Systems. 2011"},{"key":"6048_CR20","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1016\/j.scico.2013.09.019","volume":"80","author":"A Classen","year":"2014","unstructured":"Classen A, Cordy M, Heymans P, Legay A, Schobbens P Y. Formal semantics, modular specification, and symbolic verification of productline behaviour. Science of Computer Programming, 2014, 80: 416\u2013439","journal-title":"Science of Computer Programming"},{"issue":"2","key":"6048_CR21","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M R Prasad","year":"2005","unstructured":"Prasad M R, Biere A, Gupta A. A survey of recent advances in SATbased formal verification. International Journal on Software Tools for Technology Transfer, 2005, 7(2): 156\u2013173","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"6048_CR22","first-page":"193","volume-title":"Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere A, Cimatti A, Clarke E M, Zhu Y. Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems. 1999, 193\u2013207"},{"key":"6048_CR23","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/10722167_36","volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification","author":"O Shtrichman","year":"2000","unstructured":"Shtrichman O. Tuning SAT checkers for bounded model checking. In: Proceedings of the 12th International Conference on Computer Aided Verification. 2000, 480\u2013494"},{"key":"6048_CR24","first-page":"672","volume-title":"Proceedings of the International Conference on Software Engineering","author":"M Cordy","year":"2012","unstructured":"Cordy M, Classen A, Perrouin G, Schobbens P Y, Heymans P, Legay A. Simulation-based abstractions for software product-line model checking. In: Proceedings of the International Conference on Software Engineering. 2012, 672\u2013682"},{"key":"6048_CR25","first-page":"372","volume-title":"Proceedings of the 26th IEEE\/ACM International Conference on Automated Software Engineering","author":"S Apel","year":"2011","unstructured":"Apel S, Speidel H, Wendler P, Rheinv A, Beyer D. Detection of feature interactions using feature-aware verification. In: Proceedings of the 26th IEEE\/ACM International Conference on Automated Software Engineering. 2011, 372\u2013375"},{"key":"6048_CR26","first-page":"482","volume-title":"Proceedings of the International Conference on Software Engineering","author":"S Apel","year":"2013","unstructured":"Apel S, Rhein A V, Wendler P, Gr\u00f6\u00dflinger A, Beyer D. Strategies for product-line verification: case studies and experiments. In: Proceedings of the International Conference on Software Engineering. 2013, 482\u2013491"},{"key":"6048_CR27","first-page":"168","volume-title":"Jensen K, Podelski A, eds. Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag","author":"E Clarke","year":"2004","unstructured":"Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programs. In: Jensen K, Podelski A, eds. Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2004, 168\u2013176"},{"issue":"4","key":"6048_CR28","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n N, S\u00f6rensson N. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 2003, 89(4): 543\u2013560","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6048_CR29","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Giunchiglia E, Tacchella A, eds. Theory and Applications of Satisfiability Testing. Berlin: Springer-Verlag","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n N, S\u00f6rensson N. An extensible SAT-solver. In: Giunchiglia E, Tacchella A, eds. Theory and Applications of Satisfiability Testing. Berlin: Springer-Verlag, 2004, 502\u2013518"},{"issue":"2\u20134","key":"6048_CR30","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere A. PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation, 2008, 4(2\u20134): 75\u201397","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"4","key":"6048_CR31","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-24622-0_9","volume":"2937","author":"E Clarke","year":"2004","unstructured":"Clarke E, Kroening D, Ouaknine J, Strichman O. Completeness and complexity of bounded model checking. Lecture Notes in Computer Science, 2004, 2937(4): 85\u201396","journal-title":"Lecture Notes in Computer Science"},{"key":"6048_CR32","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"K L McMillan","year":"2002","unstructured":"McMillan K L. Applying SAT methods in unbounded symbolic model checking. In: Proceedings of the International Conference on Computer Aided Verification. 2002, 250\u2013264"},{"key":"6048_CR33","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G. Checking safety properties using induction and a SAT-solver. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design. 2000, 127\u2013144"},{"key":"6048_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume":"2725","author":"K L McMillan","year":"2003","unstructured":"McMillan K L. Interpolation and sat-based model checking. Lecture Notes in Computer Science, 2003, 2725: 1\u201313","journal-title":"Lecture Notes in Computer Science"},{"issue":"1","key":"6048_CR35","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. Science of Computer Programming, 2001, 41(1): 53\u201384","journal-title":"Science of Computer Programming"},{"key":"6048_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K L McMillan","year":"1993","unstructured":"McMillan K L. Symbolic Model Checking. Boston, MA: Springer US, 1993"},{"key":"6048_CR37","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-45652-X_11","volume-title":"Proceedings of the 2nd International Conference on Software Product Lines","author":"M Mannion","year":"2002","unstructured":"Mannion M. Using first-order logic for product line model validation. In: Proceedings of the 2nd International Conference on Software Product Lines. 2002, 176\u2013187"},{"key":"6048_CR38","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/11554844_3","volume-title":"Proceedings of the 9th International Software Product Lines Conference","author":"D Batory","year":"2005","unstructured":"Batory D. Feature models, grammars, and propositional formulas. In: Proceedings of the 9th International Software Product Lines Conference. 2005, 7\u201320"},{"key":"6048_CR39","first-page":"231","volume-title":"Proceedings of the 13th International Software Product Line Conference","author":"M Mendonca","year":"2009","unstructured":"Mendonca M, Wasowski A, Czarnecki K. SAT-based analysis of feature models is easy. In: Proceedings of the 13th International Software Product Line Conference. 2009, 231\u2013240"},{"issue":"2","key":"6048_CR40","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A Biere","year":"2002","unstructured":"Biere A, Artho C, Schuppan V. Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science, 2002, 66(2): 160\u2013177","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6048_CR41","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Proceedings of the International Conference on 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: Proceedings of the International Conference on Computer Aided Verification. 2002, 359\u2013364"},{"issue":"1","key":"6048_CR42","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1023\/B:AUSE.0000049208.84702.84","volume":"12","author":"R J Hall","year":"2005","unstructured":"Hall R J. Fundamental nonmodularity in electronic mail. Automated Software Engineering, 2005, 12(1): 41\u201379","journal-title":"Automated Software Engineering"},{"key":"6048_CR43","volume-title":"Modelling with FTS: a collection of illustrative examples","author":"A Classen","year":"2010","unstructured":"Classen A. Modelling with FTS: a collection of illustrative examples. Technical Report P-CS-TR SPLMC-00000001. 2010"},{"key":"6048_CR44","first-page":"193","volume-title":"Proceedings of the 12th International Conference on Software Product Line","author":"A Fantechi","year":"2008","unstructured":"Fantechi A, Gnesi S. Formal modeling for product families engineering. In: Proceedings of the 12th International Conference on Software Product Line. 2008, 193\u2013202"},{"key":"6048_CR45","volume-title":"Cardiac Pacing and ICDs","author":"K A Ellenbogen","year":"2008","unstructured":"Ellenbogen K A, Wood M A. Cardiac Pacing and ICDs. New York: John Wiley & Sons, 2008"},{"issue":"5","key":"6048_CR46","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. International Journal on Software Tools for Technology Transfer, 2012, 14(5): 589\u2013612","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"6048_CR47","first-page":"146","volume-title":"Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation","author":"P t Asirelli","year":"2012","unstructured":"Asirelli P, ter Beek M H, Fantechi A, Gnesi S. A compositional framework to derive product line behavioural descriptions. In: Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. 2012, 146\u2013161"},{"key":"6048_CR48","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/3-540-40922-X_22","volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design","author":"A Gupta","year":"2000","unstructured":"Gupta A, Yang Z, Ashar P, Gupta A. SAT-based image computation with application in reachability analysis. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design. 2000, 391\u2013408"},{"key":"6048_CR49","first-page":"510","volume-title":"Proceedings of IEEE\/ACMInternational Conference on Computer-aided design","author":"M K Ganai","year":"2004","unstructured":"Ganai M K, Gupta A, Ashar P. Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: Proceedings of IEEE\/ACMInternational Conference on Computer-aided design. 2004, 510\u2013517"},{"key":"6048_CR50","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/RE.2006.23","volume-title":"Proceedings of the 14th IEEE International Conference on Requirements Engineering","author":"P Schobbens","year":"2006","unstructured":"Schobbens P, Heymans P, Trigaux J C. Feature diagrams: a survey and a formal semantics. In: Proceedings of the 14th IEEE International Conference on Requirements Engineering. 2006, 139\u2013148"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-016-6048-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-016-6048-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-016-6048-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,15]],"date-time":"2022-08-15T04:35:00Z","timestamp":1660538100000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-016-6048-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,7]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4]]}},"alternative-id":["6048"],"URL":"https:\/\/doi.org\/10.1007\/s11704-016-6048-7","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,2,7]]},"assertion":[{"value":"24 January 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 February 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}