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

M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification, LICS'86, pp.332-344, 1986.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-263, 1986.
DOI : 10.1145/5397.5399

. Raskin, Model checking lots of systems: efficient verification of temporal properties in software product lines, Proceedings of ICSE 32, ser. ICSE '10, pp.335-344, 2010.

A. Classen, P. Heymans, P. Schobbens, and A. Legay, Symbolic model checking of software product lines, Proceeding of the 33rd international conference on Software engineering, ICSE '11, pp.321-330, 2011.
DOI : 10.1145/1985793.1985838
URL : https://hal.archives-ouvertes.fr/hal-01087657

A. Classen, Modelling and model checking variabilityintensive systems, 2011.

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

E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic, Logic of Programs, ser. LNCS, pp.52-71, 1981.

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

G. Bruns, A practical technique for process abstraction, Proceedings of the 4th International Conference on Concurrency Theory, ser. CONCUR '93, pp.37-49, 1993.
DOI : 10.1007/3-540-57208-2_4

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

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

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, Computers and Digital Techniques, pp.1-10, 1983.
DOI : 10.1049/ip-e.1983.0001

D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel, Learning operational requirements from goal models, 2009 IEEE 31st International Conference on Software Engineering, pp.265-275, 2009.
DOI : 10.1109/ICSE.2009.5070527

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

P. Asirelli, M. H. 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

M. Sassolas, M. Chechik, and S. Uchitel, Exploring inconsistencies between modal transition systems, Software & Systems Modeling, vol.35, issue.3, pp.117-142, 2011.
DOI : 10.1007/s10270-010-0148-x
URL : https://hal.archives-ouvertes.fr/hal-01161870

K. G. Larsen, U. Nyman, and A. Wasowski, Modal I/O Automata for Interface and Product Line Theories, ESOP, pp.64-79, 2007.
DOI : 10.1007/978-3-540-71316-6_6
URL : http://vbn.aau.dk/ws/files/16109957/ESOP2007withappendix.pdf

K. Lauenroth, S. Thning, and K. Pohl, Model Checking of Domain Artifacts in Product Line Engineering, 2009 IEEE/ACM International Conference on Automated Software Engineering, pp.269-280, 2009.
DOI : 10.1109/ASE.2009.16

C. Ghezzi and A. M. Sharifloo, Verifying nonfunctional properties of software product lines: Towards an efficient approach using parametric model checking, Proceedings of the 15th International Software Product Line Conference, ser. SPLC'11, pp.170-174, 2011.

F. Cassez, M. D. Ryan, and P. Schobbens, Proving feature non-interaction with Alternating-Time Temporal Logic, Language Constructs for Describing Features ? proceedings of the FIREworks workshop, 2001.
DOI : 10.1007/978-1-4471-0287-8_6

K. Fisler and S. Krishnamurthi, Modular verification of collaboration-based software designs, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, ser. ESEC/FSE-9, pp.152-163, 2001.

S. Krishnamurthi, K. Fisler, and M. Greenberg, Verifying aspect advice modularly, SIGSOFT '04/FSE-12: Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, pp.137-146, 2004.
DOI : 10.1145/1041685.1029916
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.8124

H. C. Li, S. Krishnamurthi, and K. Fisler, Interfaces for modular feature verification, Proceedings 17th IEEE International Conference on Automated Software Engineering,, pp.195-204, 2002.
DOI : 10.1109/ASE.2002.1115013

J. Liu, S. Basu, and R. R. Lutz, Compositional model checking of software product lines using variation point obligations, Automated Software Engineering, vol.26, issue.8, pp.39-76, 2011.
DOI : 10.1007/s10515-010-0075-7

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

J. F. Groote and F. Va, An efficient algorithm for branching bisimulation and stuttering equivalence, Proceedings of the seventeenth international colloquium on Automata, languages and programming, pp.626-638, 1990.
DOI : 10.1007/BFb0032063

G. Frehse, Compositional verification of hybrid systems using simulation relations, 2005.