A. Albarghouthi, Y. Li, A. Gurfinkel, and M. Chechik, Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification, CAV, pp.672-678, 2012.
DOI : 10.1007/978-3-642-31424-7_48

S. Apel, H. Speidel, P. Wendler, A. Von-rhein, and D. Beyer, Detection of feature interactions using feature-aware verification, 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), pp.372-375, 2011.
DOI : 10.1109/ASE.2011.6100075

S. Apel, A. Von-rhein, P. Wendler, A. Größlinger, and D. Beyer, Strategies for product-line verification: Case studies and experiments, 2013 35th International Conference on Software Engineering (ICSE), pp.482-491, 2013.
DOI : 10.1109/ICSE.2013.6606594

P. Asirelli, M. H. Ter-beek, A. Fantechi, and S. Gnesi, Formal Description of Variability in Product Families, 2011 15th International Software Product Line Conference, pp.130-139, 2011.
DOI : 10.1109/SPLC.2011.34

C. Baier and J. Katoen, Principles of Model Checking, 2007.

D. Beyer, Second competition on software verification -(summary of sv-comp 2013), TACAS '13, pp.594-609, 2013.

D. Beyer and M. E. Keremoglu, CPAchecker: A Tool for Configurable Software Verification, CAV '11, pp.184-190, 2011.
DOI : 10.1007/978-3-540-31980-1_40

Q. Boucher, A. Classen, P. Heymans, A. Bourdoux, and L. Demonceau, Tag and prune, Proceedings of the IEEE/ACM international conference on Automated software engineering, ASE '10, pp.333-336, 2010.
DOI : 10.1145/1858996.1859064

G. Bruns and P. Godefroid, Model Checking with Multi-valued Logics, ICALP '04, pp.281-293, 2004.
DOI : 10.1007/978-3-540-27836-8_26

M. Chechik, B. Devereux, and A. Gurfinkel, Model-checking infinite state-space systems with fine-grained abstractions using spin, SPIN '01, pp.16-36, 2001.

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement, Computer Aided Verification, pp.154-169
DOI : 10.1109/time.2003.1214874
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.407

E. Clarke, O. Grumberg, and D. Peled, Model Checking, 1999.

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design, vol.25, issue.2/3, pp.105-127, 2004.
DOI : 10.1023/B:FORM.0000040025.89719.f3

A. Classen, M. Cordy, P. Heymans, A. Legay, and P. Schobbens, Model checking software product lines with SNIP, International Journal on Software Tools for Technology Transfer, vol.41, issue.1, pp.589-612, 2012.
DOI : 10.1007/s10009-012-0234-1
URL : https://hal.archives-ouvertes.fr/hal-00717956

A. Classen, M. Cordy, P. Heymans, P. Schobbens, and A. Legay, Snip: An efficient model checker for software product lines, 2011.

A. Classen, M. Cordy, P. Schobbens, P. Heymans, A. Legay et al., Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking, IEEE Transactions on Software Engineering, vol.39, issue.8, pp.1069-1089, 2013.
DOI : 10.1109/TSE.2012.86

A. Classen, P. Heymans, P. Schobbens, and A. Legay, Symbolic model checking of software product lines Model checking lots of systems: efficient verification of temporal properties in software product lines, ICSE'11 ICSE'10, pp.321-330, 2010.

P. C. Clements and L. Northrop, Software Product Lines: Practices and Patterns. SEI Series in Software Engineering, 2001.

M. Cordy, A. Classen, P. Heymans, P. Schobbens, and A. Legay, Managing evolution in software product lines, Proceedings of the Sixth International Workshop on Variability Modeling of Software-Intensive Systems, VaMoS '12, pp.183-191, 2012.
DOI : 10.1145/2110147.2110168
URL : https://hal.archives-ouvertes.fr/hal-00718216

M. Cordy, A. Classen, G. Perrouin, P. Heymans, P. Schobbens et al., Simulation-based abstractions for software product-line model checking, 2012 34th International Conference on Software Engineering (ICSE), pp.672-682, 2012.
DOI : 10.1109/ICSE.2012.6227150
URL : https://hal.archives-ouvertes.fr/hal-01087659

M. Cordy, P. Schobbens, P. Heymans, and A. Legay, ProVeLines, Proceedings of the 17th International Software Product Line Conference co-located workshops on, SPLC '13 Workshops, pp.141-146, 2013.
DOI : 10.1145/2499777.2499781
URL : https://hal.archives-ouvertes.fr/hal-00931670

W. Craig, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, The Journal of Symbolic Logic, vol.14, issue.03, pp.269-285, 1957.
DOI : 10.2307/2963594

S. Falke, F. Merz, and C. Sinz, The bounded model checker LLBMC, 2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp.706-709, 2013.
DOI : 10.1109/ASE.2013.6693138

D. Fischbein, S. Uchitel, and V. Braberman, A foundation for behavioural conformance in software product line architectures, Proceedings of the ISSTA 2006 workshop on Role of software architecture for testing and analysis , ROSATEA '06, pp.39-48, 2006.
DOI : 10.1145/1147249.1147254

S. Graf and H. Sa¨?disa¨?di, Construction of abstract state graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, CAV '97, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

A. Gruler, M. Leucker, and K. Scheidemann, Modeling and Model Checking Software Product Lines, FMOODS'08, pp.113-131, 2008.
DOI : 10.1007/978-3-540-68863-1_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.149.5754

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, 2004.
DOI : 10.1109/32.588521

K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson, Feature-oriented domain analysis (FODA) feasibility study, 1990.

J. Kramer, J. Magee, M. Sloman, and A. Lister, CONIC: an integrated approach to distributed computer control systems, IEE Proceedings E Computers and Digital Techniques, vol.130, issue.1, pp.1-10, 1983.
DOI : 10.1049/ip-e.1983.0001

J. Liebig, A. Von-rhein, C. Kästner, S. Apel, J. Dörre et al., Scalable analysis of variable software, Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pp.81-91, 2013.
DOI : 10.1145/2491411.2491437

R. Milner, An algebraic definition of simulation between programs, 1971.

J. Morse, L. Cordeiro, D. Nicole, and B. Fischer, Handling unbounded loops with esbmc 1.20 (competition contribution), TACAS, pp.619-622, 2013.
DOI : 10.1007/978-3-642-36742-7_47

M. Plath and M. Ryan, Feature integration using a feature construct, Science of Computer Programming, vol.41, issue.1, pp.53-84, 2001.
DOI : 10.1016/S0167-6423(00)00018-6

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

H. Post and C. Sinz, Configuration Lifting: Verification meets Software Configuration, 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pp.347-350, 2008.
DOI : 10.1109/ASE.2008.45
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.570.9106

P. Schobbens, P. Heymans, J. Trigaux, and Y. Bontemps, Feature Diagrams: A Survey and a Formal Semantics, 14th IEEE International Requirements Engineering Conference (RE'06), pp.139-148, 2006.
DOI : 10.1109/RE.2006.23