R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

S. Bornot and J. Sifakis, An algebraic framework for urgency. Information and Computation, 2000.

I. Dragomir, I. Ober, and D. Lesens, A case study in formal system engineering with SysML, Engineering of Complex Computer Systems (ICECCS), 2012 17th IEEE International Conference on, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01151016

E. , A. Emerson, and E. M. Clarke, Characterizing correctness properties of parallel programs using fixpoints, ICALP, 1980.

K. Dilsun, N. Kaynar, and . Lynch, Roberto Segala, and Frits Vaandrager. The Theory of Timed I/O Automata -Second Edition, 2010.

K. Larsen, U. Nyman, and A. Wasowski, Interface Input/Output Automata, FM 2006: Formal Methods, 2006.
DOI : 10.1007/11813040_7

R. Inc, Software Considerations in Airborne Systems and Equipment Certification, 2011.

B. Meyer, Applying 'design by contract', Computer, vol.25, issue.10, pp.40-51, 1992.
DOI : 10.1109/2.161279

D. L. Parnas and D. M. Weiss, Active design reviews: Principles and practices, Proceedings, 8th International Conference on Software Engineering (ICSE), 1985.
DOI : 10.1016/0164-1212(87)90025-2

J. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR, Symposium on Programming, pp.337-351, 1982.
DOI : 10.1007/3-540-11494-7_22

S. Quinton, Design, vérification et implémentation de systèmessystèmes`systèmesà composants, 2011.

S. Quinton, S. Graf, and R. Passerone, Contract-Based Reasoning for Component Systems with Complex Interactions, 2010.

F. Wang, Symbolic Simulation-Checking of Dense-Time Automata, FORMATS, pp.352-368, 2007.
DOI : 10.1007/978-3-540-75454-1_25

N. Agrawal, V. Prabhakaran, T. Wobber, J. Davis, M. Manasse et al., Design tradeoffs for SSD performance, USENIX 2008 Annual Technical Conference on Annual Technical Conference, pp.57-70, 2008.

R. Alur, R. Grosu, Y. Hur, V. Kumar, and I. Lee, Modular Specification of Hybrid Systems in Charon, Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control, HSCC '00, pp.6-19, 2000.
DOI : 10.1007/3-540-46430-1_5

F. André, E. Daubert, N. Grégory, B. Morin, and O. Barais, F4Plan: An Approach to Build Efficient Adaptation Plans, MobiQuitous. ACM, 2010.
DOI : 10.1007/978-3-540-89897-9_5

S. Bagchi, Nano-kernel: A Dynamically Reconfigurable Kernel for WSN, Proceedings of the 1st International ICST Conference on Mobile Wireless Middleware, Operating Systems and Applications, pp.1-10, 2007.
DOI : 10.4108/ICST.MOBILWARE2008.2500

. Autohome, An Autonomic Management Framework for Pervasive Home Applications, ACM Trans. Auton. Adapt. Syst, vol.68, pp.1-8, 2011.

S. Burmester, H. Giese, and O. Oberschelp, HYBRID UML COMPONENTS FOR THE DESIGN OF COMPLEX SELF-OPTIMIZING MECHATRONIC SYSTEMS, INFORMATICS IN CONTROL, AUTOMATION AND ROBOTICS I, pp.281-288, 2006.
DOI : 10.1007/1-4020-4543-3_34

D. Cassou, E. Balland, C. Consel, and J. Lawall, Leveraging software architectures to guide and verify the development of sense/compute/control applications, Proceeding of the 33rd international conference on Software engineering, ICSE '11, pp.431-440, 2011.
DOI : 10.1145/1985793.1985852
URL : https://hal.archives-ouvertes.fr/inria-00537789

E. M. Dashofy, A. Van-der-hoek, and R. N. Taylor, An infrastructure for the rapid development of XML-based architecture description languages, Proceedings of the 24th international conference on Software engineering , ICSE '02, pp.266-276, 2002.
DOI : 10.1145/581372.581374

P. David, T. Ledoux, M. Léger, and T. Coupaye, FPath and FScript: Language support for navigation and reliable reconfiguration of Fractal architectures, annals of telecommunications - annales des t??l??communications, vol.7, issue.3, pp.45-63, 2009.
DOI : 10.1007/s12243-008-0073-y
URL : https://hal.archives-ouvertes.fr/hal-00468474

J. Eker, J. Janneck, E. A. Lee, J. Liu, X. Liu et al., Taming heterogeneity - the Ptolemy approach, Proceedings of the IEEE, pp.127-144, 2003.
DOI : 10.1109/JPROC.2002.805829

C. Escoffier, R. S. Hall, and P. Lalanda, iPOJO: an Extensible Service-Oriented Component Framework, IEEE International Conference on Services Computing (SCC 2007), pp.474-481, 2007.
DOI : 10.1109/SCC.2007.74

J. Fassino, J. Stefani, J. L. Lawall, and G. Muller, Think: A Software Framework for Component-based Operating System Kernels, General Track of the annual conference on USENIX Annual Technical Conference, pp.73-86, 2002.

F. Fleurey, B. Morin, and A. Solberg, A Model-Driven Approach to Develop Adaptive Firmwares [16] T. Henzinger. Masaccio: A formal model for embedded components, SEAMS'11@ICSE: Workshop on Software Engineering for Adaptive and Self-Managing Systems Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics, volume 1872 of Lecture Notes in Computer Science, pp.549-563, 2000.

E. Höfig, P. H. Deussen, and I. Schieferdecker, On the performance of UML state machine interpretation at runtime, 6th international symposium on Software engineering for adaptive and self-managing systems (SEAMS '11), pp.118-127, 2011.

R. Johnson and B. Woolf, The Type Object Pattern, 1997.

E. Jovanov, A. Milenkovï, A. , S. Basham, D. Clark et al., Reconfigurable intelligent sensors for health monitoring: a case study of pulse oximeter sensor, The 26th Annual International Conference of the IEEE Engineering in Medicine and Biology Society, pp.4759-4762, 2004.
DOI : 10.1109/IEMBS.2004.1404317

J. O. Kephart and D. M. Chess, The vision of autonomic computing, Computer, vol.36, issue.1, pp.41-50, 2003.
DOI : 10.1109/MC.2003.1160055

N. Medvidovic and R. N. Taylor, A classification and comparison framework for software architecture description languages, IEEE Transactions on Software Engineering, vol.26, issue.1, pp.70-93, 2000.
DOI : 10.1109/32.825767
URL : https://hal.archives-ouvertes.fr/hal-00444077

B. Morin, O. Barais, J. Jézéquel, F. Fleurey, and A. Solberg, Models@ Run.time to Support Dynamic Adaptation, Computer, vol.42, issue.10, pp.4244-51, 2009.
DOI : 10.1109/MC.2009.327

B. Morin, O. Barais, G. Nain, and J. Jezequel, Taming Dynamically Adaptive Systems using models and aspects, 2009 IEEE 31st International Conference on Software Engineering, 2009.
DOI : 10.1109/ICSE.2009.5070514

E. D. Nitto, C. Ghezzi, A. Metzger, M. P. Papazoglou, and K. Pohl, A journey to highly dynamic, self-adaptive service-based applications, Automated Software Engineering, vol.10, issue.3, pp.3-4313, 2008.
DOI : 10.1007/s10515-008-0032-x

A. Ranganathan, S. Chetan, J. Al-muhtadi, R. H. Campbell, and M. D. Mickunas, Olympus: A High-Level Programming Model for Pervasive Computing Environments, Third IEEE International Conference on Pervasive Computing and Communications, pp.7-16, 2005.
DOI : 10.1109/PERCOM.2005.26

J. S. Rellermeyer, O. Riva, and G. Alonso, AlfredO: An Architecture for Flexible Interaction with Electronic Devices, 9th ACM/IFIP/USENIX International Conference on Middleware, Middleware '08, pp.22-41, 2008.
DOI : 10.1145/571985.572008

M. Román, C. Hess, R. Cerqueira, A. Ranganathan, R. H. Campbell et al., A middleware infrastructure for active spaces, IEEE Pervasive Computing, vol.1, issue.4, pp.74-83, 2002.
DOI : 10.1109/MPRV.2002.1158281

W. Schäfer and H. Wehrheim, Graph transformations and model-driven engineering. chapter Model-driven development with Mechatronic UML, pp.533-554

L. Seinturier, P. Merle, R. Rouvoy, D. Romero, V. Schiavoni et al., A Component-Based Middleware Platform for Reconfigurable Service-Oriented Architectures. Software: Practice and Experience, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00567442

H. Singh, M. Lee, G. Lu, N. Bagherzadeh, F. J. Kurdahi et al., MorphoSys: an integrated reconfigurable system for data-parallel and computation-intensive applications, IEEE Transactions on Computers, vol.49, issue.5, pp.465-481, 2000.
DOI : 10.1109/12.859540

T. Stauner, A. Pretschner, and I. Péter, Approaching a discrete-continuous uml: Tool support and formalization, Workshop of the pUML-Group on Practical UML-Based Rigorous Development Methods -Countering or Integrating the eXtremists, pp.242-257, 2001.

R. Van-ommering, F. Van-der-linden, J. Kramer, and J. Magee, The Koala component model for consumer electronics software, Computer, vol.33, issue.3, pp.78-85, 2000.
DOI : 10.1109/2.825699

M. Acher, A. Cleve, G. Perrouin, P. Heymans, C. Vanbeneden et al., On extracting feature models from product descriptions, Proceedings of the Sixth International Workshop on Variability Modeling of Software-Intensive Systems, VaMoS '12, pp.45-54, 2012.
DOI : 10.1145/2110147.2110153
URL : https://hal.archives-ouvertes.fr/hal-00718467

J. Bézivin and O. Gerbé, Towards a precise definition of the OMG/MDA framework, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp.273-280, 2001.
DOI : 10.1109/ASE.2001.989813

R. Chenouard and F. Jouault, Automatically Discovering Hidden Transformation Chaining Constraints, Model Driven Engineering Languages and Systems, pp.92-106, 2009.
DOI : 10.1007/11754602_9
URL : https://hal.archives-ouvertes.fr/hal-00460761

J. Cordy, Eating our own Dog Food: DSLs for Generative and Transformational Engineering, GPCE, 2009.

A. Etien, V. Aranega, X. Blanc, and R. Paige, Chaining model transformations, Proceedings of the First Workshop on the Analysis of Model Transformations, AMT '12, 2012.
DOI : 10.1145/2432497.2432500

A. Etien, A. Muller, T. Legrand, and X. Blanc, Combining independent model transformations, Proceedings of the 2010 ACM Symposium on Applied Computing, SAC '10, pp.2239-2345, 2010.
DOI : 10.1145/1774088.1774557
URL : https://hal.archives-ouvertes.fr/inria-00516708

. Dekeyser, A Model Driven Design Framework for Massively Parallel Embedded Systems, ACM Transactions on Embedded Computing Systems, vol.10, issue.4, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00637595

C. Kyo, S. G. Kang, J. A. Cohen, W. E. Hess, A. Novak et al., Feature-Oriented Domain Analysis (FODA) -Feasibility Study The Software Engineering Institute, 1990.

R. Lotufo, S. She, T. Berger, K. Czarnecki, and A. Wasowski, Evolution of the Linux Kernel Variability Model, Lecture Notes in Computer Science, vol.6287, pp.136-150, 2010.
DOI : 10.1007/978-3-642-15579-6_10

T. Mens, G. Taentzer, and O. Runge, Detecting Structural Refactoring Conflicts Using Critical Pair Analysis, Electronic Notes in Theoretical Computer Science, vol.127, issue.3, pp.113-128, 2005.
DOI : 10.1016/j.entcs.2004.08.038

J. Miller and J. Mukerji, MDA Guide Version 1.0.1, Object Management Group, 2003.

J. Oldevik, Transformation Composition Modelling Framework, Proceedings of the Distributed Applications and Interoperable Systems Conference, pp.108-114, 2005.
DOI : 10.1007/11498094_10

H. Ossher, W. Harrison, and P. Tarr, Software engineering tools and environments, Proceedings of the conference on The future of Software engineering , ICSE '00, pp.261-277, 2000.
DOI : 10.1145/336512.336569

J. Pilgrim, B. Vanhooff, I. Schulz-gerlach, and Y. Berbers, Constructing and Visualizing Transformation Chains, Proceedings of the European conference on Model Driven Architecture, pp.17-32, 2008.
DOI : 10.1007/978-3-540-69100-6_2

E. José, D. Rivera, F. Ruiz-gonzalez, J. Lopez-romero, A. Bautista et al., Orchestrating ATL Model Transformations, Proc. of MtATL, pp.34-46, 2009.

C. Douglas and . Schmidt, Guest Editor's Introduction: Model-Driven Engineering, IEEE Computer, vol.39, issue.2, pp.25-31, 2006.

B. Selic, The pragmatics of model-driven development, IEEE Software, vol.20, issue.5, pp.19-25, 2003.
DOI : 10.1109/MS.2003.1231146

S. She, R. Lotufo, T. Berger, A. Wasowski, and K. Czarnecki, Reverse engineering feature models, Proceeding of the 33rd international conference on Software engineering, ICSE '11, pp.461-470, 2011.
DOI : 10.1145/1985793.1985856

B. Vanhooff, D. Ayed, and Y. Berbers, A Framework for Transformation Chain Development Processes, Proceedings of the ECMDA Composition of Model Transformations Workshop, pp.3-8, 2006.

B. Vanhooff and Y. Berbers, Breaking Up the Transformation Chain, Proceedings of the Best Practices for Model-Driven Software Development at OOPSLA 2005, 2005.

D. Wagelaar, R. Van-der-straeten, and D. Deridder, Module Superimposition: a Composition Technique for Rule-based Model Transformation Languages . Software and Systems Modeling, 2009.

H. Han and T. Tokuda, WIKE: A Web Information/Knowledge Extraction System for Web Service Generation, 2008 Eighth International Conference on Web Engineering, pp.354-357, 2008.
DOI : 10.1109/ICWE.2008.30

R. Lee, A. Harikumar, C. Chiang, H. Yang, H. Kim et al., A framework for dynamically converting components to web services, Proc. of SERA'05, 2005.

A. Marinho, L. Murta, and C. , Werner Extending a Software Component Repository to Provide Services, Proc. of ICSR'09. Falls Church, pp.258-268, 2009.

C. Tibermacine and M. L. Kerdoudi, Migrating Component-Based Web Applications to Web Services: Towards Considering a "Web Interface as a Service", 2012 IEEE 19th International Conference on Web Services, 2012.
DOI : 10.1109/ICWS.2012.24

L. Barguñó, C. Creus, G. Godoy, F. Jacquemard, and C. Vacher, The Emptiness Problem for Tree Automata with Global Constraints, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.263-272, 2010.
DOI : 10.1109/LICS.2010.28

E. Filiot, J. Talbot, and S. Tison, TREE AUTOMATA WITH GLOBAL CONSTRAINTS, International Journal of Foundations of Computer Science, vol.21, issue.04, pp.571-596, 2010.
DOI : 10.1142/S012905411000743X
URL : https://hal.archives-ouvertes.fr/inria-00292027

P. Héam, V. Hugot, and O. Kouchnarenko, On Positive TAGED with a Bounded Number of Constraints, CIAA, pp.329-336, 2012.
DOI : 10.1007/978-3-642-31606-7_29

F. Jacquemard, F. Klay, and C. Vacher, Rigid tree automata and applications, Information and Computation, vol.209, issue.3, pp.486-512, 2011.
DOI : 10.1016/j.ic.2010.11.015
URL : https://hal.archives-ouvertes.fr/inria-00578820

G. Jesper, M. Henriksen, K. Mukund, M. A. Narayan-kumar, P. S. Sohoni et al., A theory of regular msc languages. Information and Computation/information and Control, pp.1-38, 2005.

K. Lodaya and P. Weil, Series-parallel posets: Algebra, automata and languages, STACS98, Lecture Nodes in Computer Science, pp.555-565, 1998.
DOI : 10.1007/BFb0028590

R. Morin, Recognizable Sets of Message Sequence Charts, STACS 2002, pp.523-534, 2002.
DOI : 10.1007/3-540-45841-7_43

R. Vaughan and . Pratt, Modelling concurrency with partial orders, International Journal of Parallel Programming, vol.15, issue.1, pp.33-71, 1986.

F. Bongiovanni and L. Henrio, A Mechanized Model for CAN Protocols, 16th International Conference on Fundamentals of Software Engineering (FASE'13), 2013.
DOI : 10.1007/978-3-642-37057-1_20
URL : https://hal.archives-ouvertes.fr/hal-00802006

A. Gupta, O. D. Sahin, D. Agrawal, and A. E. Abbadi, Meghdoot: Content-Based Publish/Subscribe over P2P Networks, Proceedings of the 5th ACM/IFIP/USENIX international conference on Middleware, pp.254-273, 2004.
DOI : 10.1007/3-540-45518-3_18

L. Henrio, Formal Models for Programming and Composing Correct Distributed Systems, 2012.
URL : https://hal.archives-ouvertes.fr/tel-00720022

S. Ratnasamy, P. Francis, M. Handley, R. Karp, and S. Shenker, A Scalable Content-Addressable Network, SIGCOMM, pp.161-172, 2001.

S. Ratnasamy, M. Handley, R. Karp, and S. Shenker, Application-level multicast using contentaddressable networks, 2001.

M. Cole, Algorithmic Skeletons, 1989.
DOI : 10.1007/978-1-4471-0841-2_13

S. J. Deitz, D. Callahan, B. L. Chamberlain, and L. Snyder, Global-view abstractions for user-defined reductions and scans, Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming , PPoPP '06, pp.40-47, 2006.
DOI : 10.1145/1122971.1122980

J. B. Goodenough, Exception handling: issues and a proposed notation, Communications of the ACM, vol.18, issue.12, pp.683-696, 1975.
DOI : 10.1145/361227.361230

N. Javed and F. Loulergue, Parallel Programming and Performance Predictability with Orléans Skeleton Library, International Conference on High Performance Computing and Simulation (HPCS), pp.257-263, 2011.

A. Romanovsky and J. Kienzle, Action-Oriented Exception Handling in Cooperative and Competitive Concurrent Object-Oriented Systems, Advances in Exception Handling Techniques, pp.147-164, 2001.
DOI : 10.1007/3-540-45407-1_9

H. Lin, Computing bisimulations for nite-control pi-calculus, J. Comput. Sci. Technol, vol.15, issue.1, p.19, 2000.

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, II, Information and Computation, vol.100, issue.1, p.140, 1992.
DOI : 10.1016/0890-5401(92)90009-5

U. Montanari and M. Pistore, Structured coalgebras and minimal hd-automata for the pi-calculus

R. Paige and R. E. Tarjan, Three partition renement algorithms, SIAM J. Comput, vol.16, issue.6, p.973989, 1987.

M. Pistore and D. Sangiorgi, A partition renement algorithm for the pi-calculus, Inf. Comput, vol.164, issue.2, p.264321, 2001.

F. Rosa-velardo and D. De-frutos-escrig, Decidability Results for Restricted Models of Petri Nets with Name Creation and Replication, Petri Nets, p.6382, 2009.
DOI : 10.1016/0890-5401(92)90008-4

D. L. Dill, A. J. Drexler, A. J. Hu, and C. Yang, Protocol verification as a hardware design aid, Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors, pp.522-525, 1992.
DOI : 10.1109/ICCD.1992.276232

J. Filliâtre and K. Kalyanasundaram, Functory: A Distributed Computing Library for Objective Caml, TFP, pp.65-81, 2011.
DOI : 10.1007/978-3-642-32037-8_5

S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Towards SMT Model Checking of Array-Based Systems, IJCAR, pp.67-82, 2008.
DOI : 10.1007/978-3-540-71070-7_6
URL : https://hal.archives-ouvertes.fr/inria-00576600

S. Ghilardi and S. Ranise, Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis, Logical Methods in Computer Science, vol.6, issue.4, 2010.
DOI : 10.2168/LMCS-6(4:10)2010

S. Ghilardi and S. Ranise, MCMT: A Model Checker Modulo Theories, IJCAR, pp.22-29, 2010.
DOI : 10.1007/978-3-642-14203-1_3

O. Grumberg, T. Heyman, N. Ifergan, and A. Schuster, Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation, CHARME, pp.129-145, 2005.
DOI : 10.1007/11560548_12

K. Havelund and T. Pressburger, Model checking JAVA programs using JAVA PathFinder, International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.4, pp.366-381, 2000.
DOI : 10.1007/s100090050043

T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Software Verification with BLAST, Model Checking Software, pp.624-624, 2003.
DOI : 10.1007/3-540-44829-2_17

G. J. Holzmann, The model checker spin. Software Engineering, IEEE Transactions on, vol.23, issue.5, pp.279-295, 1997.

J. Kuskin, D. Ofelt, M. Heinrich, J. Heinlein, R. Simoni et al., The Stanford FLASH multiprocessor, Computer Architecture, pp.302-313, 1994.

I. Melatti, R. Palmer, G. Sawaya, Y. Yang, R. M. Kirby et al., Parallel and distributed model checking in Eddy, International Journal on Software Tools for Technology Transfer, vol.3, issue.1, pp.13-25, 2009.
DOI : 10.1007/s10009-008-0094-x

S. Park and D. L. Dill, Protocol verification by aggregation of distributed transactions, CAV, pp.300-310, 1996.
DOI : 10.1007/3-540-61474-5_78

S. Schmitz and P. Schnoebolen, Algorithmic Aspects of WQO (Well- Quasy-Ordering) Theory. ESSLLI, 2012.

M. Talupur and M. R. Tuttle, Going with the Flow: Parameterized Verification Using Message Flows, 2008 Formal Methods in Computer-Aided Design, pp.1-10, 2008.
DOI : 10.1109/FMCAD.2008.ECP.14

M. Abadi, M. Budiu, U. Erlingsson, and J. Ligatti, Control-flow integrity principles, implementations, and applications, ACM Transactions on Information and System Security, vol.13, issue.1
DOI : 10.1145/1609956.1609960

L. Boehne, Pandora's bochs: Automatic unpacking of malware, 2008.

G. Bonfante, J. Marion, and D. Reynaud, A Computability Perspective on Self-Modifying Programs, 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009.
DOI : 10.1109/SEFM.2009.25
URL : https://hal.archives-ouvertes.fr/inria-00433472

H. Cai, Z. Shao, and A. Vaynberg, Certified self-modifying code, ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07), pp.66-77, 2007.

A. Chaudhuri, P. Naldurg, and S. Rajamani, A type system for data-flow integrity on windows vista, In ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2008.

. Datarescue, Using the universal pe unpacker plug-in included in ida pro 4.9 to unpack compressed executables, 2005.

S. Debray, K. Coogan, and G. Townsend, On the semantics of self-unpacking malware code, 2008.

A. Dinaburg, P. Royal, M. Sharif, and W. Lee, Ether, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, pp.51-62, 2008.
DOI : 10.1145/1455770.1455779

G. Erdélyi, Idapython: User scripting for a complex application, 2008.

P. Ferrie, Anti-unpacker tricks, 2008.

B. Ford and R. Cox, Vx32: lightweight user-level sandboxing on the x86, ATC'08: USENIX 2008 Annual Technical Conference on Annual Technical Conference, pp.293-306, 2008.

V. Gratzer and D. Naccache, Alien vs. Quine, IEEE Security and Privacy Magazine, vol.5, issue.2, pp.26-31, 2007.
DOI : 10.1109/MSP.2007.28

W. Guizani, J. Marion, and D. Reynaud, Server-side dynamic code analysis, 2009 4th International Conference on Malicious and Unwanted Software (MALWARE), 2009.
DOI : 10.1109/MALWARE.2009.5403017
URL : https://hal.archives-ouvertes.fr/inria-00425554

C. A. Gunter, Semantics of Programming Languages: Structures and Techniques, 1992.

F. Guo, P. Ferrie, and T. Chiueh, A Study of the Packer Problem and Its Solutions, RAID '08: Proceedings of the 11th international symposium on Recent Advances in Intrusion Detection, pp.98-115, 2008.
DOI : 10.1007/978-3-540-87403-4_6

S. Josse, Secure and advanced unpacking using computer emulation, Journal in Computer Virology, vol.3, issue.3, 2007.
DOI : 10.1007/s11416-007-0046-0

M. Gyung-kang, H. Yin, and P. Poosankam, Renovo: A hidden code extractor for packed executables, 5th ACM Workshop on Recurring Malcode, 2007.

S. C. Kleene, Introduction to Metamathematics, 1952.

M. A. Lopez, Unpacking, a hybrid approach, 2nd International CARO Workshop, 2008.

C. Luk, R. Cohn, R. Muth, H. Patil, A. Klauser et al., Pin: Building customized program analysis tools with dynamic instrumentation, Programming Language Design and Implementation (PLDI), 2005.

L. Martignoni, M. Christodorescu, and S. Jha, OmniUnpack: Fast, Generic, and Safe Unpacking of Malware, Twenty-Third Annual Computer Security Applications Conference (ACSAC 2007), pp.431-441, 2007.
DOI : 10.1109/ACSAC.2007.15

J. Mitchell, Foundations for Programming Languages, 1996.

A. Moser, C. Kruegel, and E. Kirda, Exploring Multiple Execution Paths for Malware Analysis, 2007 IEEE Symposium on Security and Privacy (SP '07), pp.231-245, 2007.
DOI : 10.1109/SP.2007.17

M. O. Myreen, Verified just-in-time compiler on x86, Proceedings of Principles of Programming Languages (POPL), 2010.

D. Quist and . Valsmith, covert debugging, circumventing software armoring techniques, Black Hat USA, 2007.

P. Royal, M. Halpin, D. Dagon, R. Edmonds, and W. Lee, PolyUnpack: Automating the Hidden-Code Extraction of Unpack-Executing Malware, 2006 22nd Annual Computer Security Applications Conference (ACSAC'06), pp.289-300, 2006.
DOI : 10.1109/ACSAC.2006.38

A. Sabelfeld and A. C. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications, vol.21, issue.1, pp.5-19, 2003.
DOI : 10.1109/JSAC.2002.806121

S. Sarkar, P. Sewell, F. Z. Nardelli, S. Owens, T. Ridge et al., The semantics of x86-cc multiprocessor machine code, POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.379-391, 2009.

M. Sharif, A. Lanzi, J. Giffin, and W. Lee, Automatic Reverse Engineering of Malware Emulators, 2009 30th IEEE Symposium on Security and Privacy, pp.94-109, 2009.
DOI : 10.1109/SP.2009.27

. Skape, Using dual-mappings to evade automated unpackers, 2008.

J. Stewart, Semi-automatic unpacking on ia-32, Defcon, 2006.

P. Vogt, F. Nentwich, N. Jovanovic, E. Kirda, C. Kruegel et al., Cross site scripting prevention with dynamic data tainting and static analysis, 2007.

D. Heng-yin, M. Song, C. Egele, E. Kruegel, and . Kirda, Panorama: capturing system-wide information flow for malware detection and analysis, CCS '07: Proceedings of the 14th ACM conference on Computer and communications security, pp.116-127, 2007.

. M. Bcf-+-12, A. Bodin, D. Charguéraud, P. Filaretti, S. Gardner et al., Flocq: A Unified Library for Proving Floating-point Algorithms in Coq, 2010.

. A. Boh12 and . Bohannon, Foundations of Web Script Security, 2012.

C. A. Charguéraud, The Optimal Fixed Point Combinator, Proceeding of the first international conference on Interactive Theorem Proving (ITP), pp.195-210, 2010.
DOI : 10.1007/978-3-642-14052-5_15

C. A. Charguéraud, TLC: a non-constructive library for coq based on typeclasses, 2010.

C. A. Charguéraud, C. R. Chugh, D. Herman, R. Jhala, C. R. Chugh et al., Pretty-big-step semantics Dependent types for javascript Nested refinements: a logic for duck typing, Proceedings of the 22nd European Symposium on Programming (ESOP) Proceedings of OOPSLA 2012 Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '12, pp.231-244, 2012.

. Eny12 and . Enyo, Enyo web site, p.2012

G. P. Gardner, S. Maffeis, and G. D. Smith, Towards a program logic for javascript, Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.31-44, 2012.

G. A. Guha, C. Saftoiu, S. Krishnamurthi, H. D. Hedin, and A. Sabelfeld, The essence of javascript. ECOOP 2010?Object- Oriented Programming Information-flow security for a core of javascript Validating lr(1) parsers, Proceedings of the 25th IEEE Computer Security Foundations Symposium, CSF 2012 Proceedings of the 21st European conference on Programming Languages and Systems, pp.126-150, 2010.

L. Z. Luo and T. Rezk, Mashic compiler: Mashup sandboxing based on inter-frame communication, IEEE Proceedings of 25th IEEE Computer Security Foundations Symposium, pp.157-170, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01353966

M. S. Maffeis, J. Mitchell, and A. Taly, An operational semantics for javascript. Programming Languages and Systems, pp.307-325, 2008.

M. S. Maffeis, J. C. Mitchell, and A. Taly, An Operational Semantics for JavaScript, 2011.
DOI : 10.1007/11601524_11

M. Mozilla, . M. Sgl06, E. Serrano, F. Gallesio, and . Loitsch, B2g wiki Hop: a language for programming the web 2.0, Proceedings of the First Dynamic Languages Symposium ACM. SO08. M. Sozeau and N. Oury. First-class type classes. Theorem Proving in Higher Order Logics, pp.975-985, 2006.

T. A. +-11, Ú. Taly, J. C. Erlingsson, M. S. Mitchell, J. Miller et al., Automated analysis of securitycritical javascript apis, Security and Privacy (SP), 2011 IEEE Symposium on, pp.363-378, 2011.

Y. D. Yu, A. Chander, N. Islam, and I. Serikov, Javascript instrumentation for browser security, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '07, pp.237-249, 2007.

. A. Zak11 and . Zakai, Emscripten: an llvm-to-javascript compiler, Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion, pp.301-312, 2011.

O. Chebaro, N. Kosmatov, A. Giorgetti, and J. Julliand, Program slicing enhances a verification technique combining static and dynamic analysis, Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC '12, pp.1284-1291, 2012.
DOI : 10.1145/2245276.2231980
URL : https://hal.archives-ouvertes.fr/hal-00746814

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, a program analysis perspective, the 10th Int. Conference on Software Engineering and Formal Methods, pp.233-247, 2012.

B. Botella, M. Delahaye, S. Hong-tuan-ha, N. Kosmatov, P. Mouy et al., Automating structural testing of C programs: Experience with PathCrawler, 2009 ICSE Workshop on Automation of Software Test, pp.70-78, 2009.
DOI : 10.1109/IWAST.2009.5069043

P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language, v1, 2012.

J. Signoles, E-ACSL: Executable ANSI/ISO C Specification Language, 2012.

M. Delahaye, N. Kosmatov, and J. Signoles, Common specification language for static and dynamic analysis of C programs, Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC '13, 2013.
DOI : 10.1145/2480362.2480593
URL : https://hal.archives-ouvertes.fr/hal-00853721

J. Signoles, E-ACSL Version 1.5-4. Implementation in Frama-C Plug-in E-ACSL version 0.1, 2012.

M. Carlier, C. Dubois, and A. Gotlieb, Constraint reasoning in focaltest, Int. Conf. on Soft. and Data Tech. (ICSOFT'10), 2010.
URL : https://hal.archives-ouvertes.fr/hal-00699233

M. Carlier, C. Dubois, and A. Gotlieb, A Certified Constraint Solver over Finite Domains, Formal Methods, pp.116-131, 2012.
DOI : 10.1007/978-3-642-32759-9_12
URL : https://hal.archives-ouvertes.fr/hal-01126135

M. Carlier, C. Dubois, and A. Gotlieb, A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest, Proc. of 6th Int. Conf. on Test&Proofs (TAP'12), 2012.
DOI : 10.1007/978-3-642-30473-6_5
URL : https://hal.archives-ouvertes.fr/hal-01126115

A. Mackworth, Consistency in networks of relations, Artificial Intelligence, vol.8, issue.1, pp.99-118, 1977.
DOI : 10.1016/0004-3702(77)90007-8

H. N. Nguyen, P. Poizat, and F. Za¨?diza¨?di, A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies, pp.2012-525, 2012.
DOI : 10.1007/978-3-642-34321-6_36
URL : https://hal.archives-ouvertes.fr/hal-01367304

Z. Qiu, X. Zhao, C. Cai, and H. Yang, Towards the theoretical foundation of choreography, Proceedings of the 16th international conference on World Wide Web , WWW '07, 2007.
DOI : 10.1145/1242572.1242704

R. Van-glabbeek and W. Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM, vol.43, issue.3, pp.555-600, 1996.
DOI : 10.1145/233551.233556

R. 1. Acher, M. Cleve, A. Collet, P. Merle, P. Duchien et al., Reverse Engineering Architectural Feature Models
DOI : 10.1002/spe.652
URL : https://hal.archives-ouvertes.fr/inria-00614984

V. Alves, C. Schwanninger, L. Barbosa, A. Rashid, P. Sawyer et al., An Exploratory Study of Information Retrieval Techniques in Domain Analysis, 2008 12th International Software Product Line Conference, pp.67-76, 2008.
DOI : 10.1109/SPLC.2008.18

P. Clements and L. Northrop, Software product lines: practices and patterns, 2001.

L. Northrop, A framework for software product line practice -version 5, Software Engineering Institute, 2011.

U. Ryssel, J. Ploennigs, and K. Kabitzsch, Automatic variation-point identification in function-block-based models, pp.23-32, 2010.

T. Ziadi, L. Frias, M. A. Da-silva, and M. Ziane, Feature Identification from the Source Code of Product Variants, 2012 16th European Conference on Software Maintenance and Reengineering, pp.417-422, 2012.
DOI : 10.1109/CSMR.2012.52
URL : https://hal.archives-ouvertes.fr/hal-01270063

R. 1. Al-msie-'deen, R. Seriai, A. D. Huchard, M. Urtado, C. Vauttier et al., An approach to recover feature models from object-oriented source code, Actes de la Journée Lignes de Produits 2012, pp.15-26, 2012.
URL : https://hal.archives-ouvertes.fr/lirmm-00808443

A. -msie-'deen, R. Seriai, A. D. Huchard, M. Urtado, C. Vauttier et al., Survey: reverse engineering feature model/features from different artefacts, Survey, vol.24, 2013.

B. Dit, M. Revelle, M. Gethers, and D. Poshyvanyk, Feature location in source code: a taxonomy and survey, Journal of Software: Evolution and Process, vol.20, issue.6, p.5395, 2012.
DOI : 10.1002/smr.567

B. Ganter and R. Wille, Formal Concept Analysis, Mathematical Foundations, 1999.

A. Marcus and J. I. Maletic, Recovering documentation-to-source-code traceability links using latent semantic indexing, 25th International Conference on Software Engineering, 2003. Proceedings., pp.125-135, 2003.
DOI : 10.1109/ICSE.2003.1201194
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.8007

A. -msie-'deen, R. Seriai, A. D. Huchard, M. Urtado, C. Vauttier et al., ArgoUML case study, 2013.

A. M. Pinna-déry, C. C. Gutierrez-rodriguez, and A. Occello, How a Patient Might Adjust his Cochlear Implant by Using a Smartphone, IADIS International Conference e-Health 2012 (e-Health'2012), 2012.

S. Mosser, M. Blay-fornarino, and L. Duchien, A Commutative Model Composition Operator to Support Software Adaptation, 8th European Conference on Modelling Foundations and Applications (ECMFA'12), pp.4-19, 2012.
DOI : 10.1007/978-3-642-31491-9_3
URL : https://hal.archives-ouvertes.fr/hal-00689706

S. Mosser, F. Fleurey, B. Morin, F. Chauvel, A. Solberg et al., SENSAPP as a Reference Platform to Support Cloud Experiments: From the Internet of Things to the Internet of Services, 2012 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2012.
DOI : 10.1109/SYNASC.2012.71

P. Hudak, A Semantic Model of Reference Counting and its Abstraction, Abstract Interpretation of Declarative Languages, pp.45-62, 1987.

P. Vasconcelos, Space Cost Analysis Using Sized Types, 2008.

D. Le-berre and A. Parrain, The Sat4j library, release 2.2 system description, Journal on Satisfiability Boolean Modeling and Computation, vol.7, pp.59-64, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00868136

I. Giurgiu, O. Riva, and G. Alonso, Dynamic Software Deployment from Clouds to Mobile Devices, Middleware, pp.394-414, 2012.
DOI : 10.1109/MPRV.2009.82

R. Kemp, N. Palmer, T. Kielmann, and H. Bal, Cuckoo: A Computation Offloading Framework for Smartphones, Mobile Computing, Applications, and Services, pp.59-79, 2012.
DOI : 10.1109/MPRV.2005.9

K. Kumar and Y. Lu, Cloud Computing for Mobile Users: Can Offloading Computation Save Energy?, Computer, vol.43, issue.4, pp.51-56, 2013.
DOI : 10.1109/MC.2010.98

H. Dedukti, Coqine et Focalide sont disponibles en ligne sur le site web de Dedukti : https://www.rocq.inria.fr/deducteam

A. Assaf and G. Burel, Translating HOL to Dedukti, Electronic Proceedings in Theoretical Computer Science, vol.186
DOI : 10.4204/EPTCS.186.8
URL : https://hal.archives-ouvertes.fr/hal-01097412

M. Boespflug and G. Burel, CoqInE : translating the calculus of inductive constructions into the lambdapi-calculus modulo, Proof Exchange for Theorem Proving?Second International Workshop, p.44, 2012.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The lambda-pi-calculus modulo as a universal proof language, Proof Exchange for Theorem Proving -Second International Workshop of CEUR Workshop Proceedings, p.28, 2012.

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, number 4583 in Lecture Notes in Computer Science, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

R. Enderlin, F. Dadeau, A. Giorgetti, and A. B. Othman, Praspel: A Specification Language for Contract-Based Testing in PHP, 23th IFIP Int. Conf. on Testing Software and Systems
DOI : 10.1007/978-3-642-24580-0_6
URL : https://hal.archives-ouvertes.fr/hal-00640279

[. Enderlin, F. Dadeau, A. Giorgetti, and F. Bouquet, Grammar-Based Testing using Realistic Domains in PHP Verification and Validation. [EGB13] Ivan Enderlin, Alain Giorgetti, and Fabrice Bouquet. A Constraint Solver for PHP Arrays, A-MOST'12, 8th Workshop on Advances in Model Based Testing, joint to the ICST'12 IEEE Int. Conf. on Software Testing CSTVA'13, 5th Workshop on Constraints in Software Testing, Verification and Analysis, joint to the ICST'13 IEEE Int. Conf. on Software Testing, Verification and Validation. Praspel Language ? Praspel = PHP Realistic Annotation and Specification Language ? Contract-based testing language expressing invariants

A. Flissi and G. Vanwormhoudt, Programmation orientée domaine pour les services télécoms : concepts, DSL et outillage, Conférence en Ingénierie du Logiciel, pp.1-6, 2012.

G. Vanwormhoudt and A. Flissi, Session-Based Role Programming for the Design of Advanced Telephony Applications, Proceedings of Distributed Applications and Interoperable Systems (DAIS'11), pp.77-91, 2011.
DOI : 10.1007/978-3-540-72883-2_1
URL : https://hal.archives-ouvertes.fr/hal-00609512