A. Alexandrakis and S. Bozapalidis, Weighted grammars and Kleene's theorem, Information Processing Letters, vol.24, issue.1, pp.1-4, 1987.
DOI : 10.1016/0020-0190(87)90190-6

M. Apel, C. Bockermann, and M. Meier, Measuring similarity of malware behavior, 2009 IEEE 34th Conference on Local Computer Networks, pp.891-898, 2009.
DOI : 10.1109/LCN.2009.5355037

G. Balakrishnan, R. Gruian, T. W. Reps, and T. Teitelbaum, CodeSurfer/x86???A Platform for Analyzing x86 Executables, Compiler Construction, 14th International Conference , CC 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 Proceedings, volume 3443 of Lecture Notes in Computer Science, pp.250-254, 2005.
DOI : 10.1007/978-3-540-31985-6_19

T. Ball, E. Bounimova, and L. De-moura, Efficient evaluation of pointer predicates with Z3 SMT solver in SLAM2, 2010.

T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani, Automatic predicate abstraction of c programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, PLDI '01, pp.203-213, 2001.

P. Bania, Generic unpacking of self-modifying, aggressive, packed binary programs. CoRR, abs/0905, p.4581, 2009.

U. Bayer, P. M. Comparetti, C. Hlauscheck, C. Kruegel, and E. Kirda, Scalable, Behavior-Based Malware Clustering, 16th Symposium on Network and Distributed System Security (NDSS), 2009.

P. Beaucamps and J. Marion, On behavioral detection, Proceedings of EICAR'09, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00758423

R. Benzmüller, S. Berkenkop, and G. Data, Half-yearly malware report, 2010.

J. Bergeron, M. Debbabi, J. Desharnais, M. Erhioui, Y. Lavoie et al., Static detection of malicious code in executable programs, Symposium on Requirements Engineering for Information Security, 2001.

J. Berstel, J. , and C. Reutenauer, Rational series and their languages, 1988.
DOI : 10.1007/978-3-642-73235-5

URL : https://hal.archives-ouvertes.fr/hal-00619791

D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, The software model checker Blast, International Journal on Software Tools for Technology Transfer, vol.2, issue.4, pp.505-525, 2007.
DOI : 10.1007/978-1-4757-3540-6

D. Beyer, T. A. Henzinger, and G. Théoduloz, Lazy Shape Analysis, CAV'06, pp.532-546, 2006.
DOI : 10.1007/11817963_48

G. Bonfante, M. Kaczmarek, and J. Marion, Architecture of a morphological malware detector, Journal in Computer Virology, vol.0, issue.4, 2008.
DOI : 10.1007/s11416-008-0102-4

URL : https://hal.archives-ouvertes.fr/inria-00330022

V. Ronald, F. Book, and . Otto, String-rewriting systems, 1993.

D. Brumley, C. Hartwig, Z. Liang, J. Newsome, D. Song et al., Automatically Identifying Trigger-based Behavior in Malware, Botnet Detection, vol.36, pp.65-88, 2008.
DOI : 10.1007/978-0-387-68768-1_4

D. Bruschi, L. Martignoni, and M. Monga, Detecting Self-mutating Malware Using Control-Flow Graph Matching, Conference on Detection of Intrusions and Malware & Vulnerability Assessment, pp.129-143, 2006.
DOI : 10.1007/11790754_8

URL : http://idea.sec.dico.unimi.it/~lorenzo/rt0906.pdf

D. R. Chase, M. Wegman, and F. K. Zadeck, Analysis of pointers and structures, ACM SIGPLAN Notices, vol.25, issue.6, pp.296-310, 1990.
DOI : 10.1145/93548.93585

F. Chen and G. Ro?u, MOP : An Efficient and Generic Runtime Verification Framework, Object-Oriented Programming, Systems, Languages and Applications(OOPSLA'07), pp.569-588, 2007.

M. Christodorescu, S. Jha, S. A. Seshia, D. Song, and R. E. Bryant, Semantics-Aware Malware Detection, 2005 IEEE Symposium on Security and Privacy (S&P'05), pp.32-46, 2005.
DOI : 10.1109/SP.2005.20

URL : http://www.cs.cmu.edu/~bryant/pubs.pdf

C. Cifuentes and K. Gough, Decompilation of binary programs, Software: Practice and Experience, vol.35, issue.7, pp.811-829, 1995.
DOI : 10.1002/spe.4380250706

E. Clarke, D. Kroening, and F. Lerda, A Tool for Checking ANSI-C Programs, Tools and Algorithms for the Construction and Analysis of Systems, pp.168-176, 2004.
DOI : 10.1007/978-3-540-24730-2_15

F. Cohen, Computer viruses, Computers & Security, vol.6, issue.1, pp.22-35, 1987.
DOI : 10.1016/0167-4048(87)90122-2

J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. P?s?reanu et al., Bandera, Proceedings of the 22nd international conference on Software engineering , ICSE '00, pp.439-448, 2000.
DOI : 10.1145/337180.337234

C. Demartini, R. Iosif, and R. Sisto, dSPIN: A Dynamic Extension of SPIN, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, pp.261-276, 1999.
DOI : 10.1007/3-540-48234-2_20

C. Devine and N. Richaud, A study of anti-virus' response to unknown threats, Proceedings of EICAR'09, 2009.

T. Dullien and R. Rolles, Graph-based comparison of executable objects, Symposium sur la Sécurité des Technologies de l'Information et des Télécommunications, 2005.

M. B. Dwyer, J. Hatcliff, M. Hoosier, V. Prasad-ranganath, R. et al., Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs, TACAS'06, pp.73-89, 2006.
DOI : 10.1007/978-3-540-31980-1_35

M. B. Dwyer, J. Hatcliff, R. , and V. Prasad-ranganath, Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented pro- grams. Formal Methods in System Design, pp.199-240, 2004.

J. Engelfriet, Z. Fülöp, and H. Vogler, Bottom-up and topdown tree series transformations, J. Autom. Lang. Comb, vol.7, pp.11-70, 2001.
DOI : 10.1007/bf01704020

J. Esparza, P. Rossmanith, and S. Schwoon, A uniform framework for problems on context-free grammars, Bulletin of the EATCS, vol.72, pp.169-177, 2000.

A. Flexeder, B. Mihaila, M. Petter, and H. Seidl, Interprocedural Control Flow Reconstruction, Proceedings of the 8th Asian conference on Programming languages and systems, APLAS'10, pp.188-203, 2010.
DOI : 10.1109/RTCSA.2000.896367

Z. Fülöp and H. Vogler, Weighted tree automata and tree transducers, Handbook of Weighted Automata, Monographs in Theoretical Computer Science. An EATCS Series, pp.313-403, 2009.

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP??2006: A Toolbox for the Construction and Analysis of Distributed Processes, Computer Aided Verification, pp.158-163, 2007.
DOI : 10.1007/978-3-540-73368-3_18

URL : https://hal.archives-ouvertes.fr/inria-00189021

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes, Tools and Algorithms for the Construction and Analysis of Systems, pp.372-387, 2011.
DOI : 10.1007/BFb0054166

URL : https://hal.archives-ouvertes.fr/inria-00583776

T. Genet, Reachability Analysis of Rewriting for Software Verification . Habilitation à diriger les recherches, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00477013

R. Gilleron and S. Tison, Regular Tree Languages and Rewrite Systems, Fundamenta Informaticae, vol.24, pp.157-176, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00538882

P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems : An Approach to the State-Explosion Problem, 1996.
DOI : 10.1007/3-540-60761-7

P. Godefroid, N. Klarlund, and K. Sen, DART, ACM SIGPLAN Notices, vol.40, issue.6, pp.213-223, 2005.
DOI : 10.1145/1064978.1065036

P. Godefroid, M. Y. Levin, and D. Molnar, Automated whitebox fuzz testing, Network Distributed Security Symposium. Internet Society, 2008.

J. F. Groote and R. Mateescu, Verification of Temporal Properties of Processes in a Setting with Data, 1998.
DOI : 10.1007/3-540-49253-4_8

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

J. Hatcliff, M. B. Dwyer, S. Laubach, and A. Muhammad, Specializing configurable systems for finite-state verification, 1998.

J. Hatcliff, M. B. Dwyer, and H. Zheng, Slicing software for model construction. Higher-Order and Symbolic Computation, pp.315-3531026599015809, 1023.

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

URL : http://ase.arc.nasa.gov/havelund/Publications/jpf-sttt.ps.Z

A. Steven, S. Hofmeyr, A. Forrest, and . Somayaji, Intrusion detection using sequences of system calls, J. Comput. Secur, vol.6, pp.151-180, 1998.

J. Gerard and . Holzmann, The SPIN Model Checker : Primer and Reference Manual, 2003.

S. Horwitz, P. Pfeiffer, and T. Reps, Dependence analysis for pointer variables, ACM SIGPLAN Notices, vol.24, issue.7, pp.28-40, 1989.
DOI : 10.1145/74818.74821

S. Horwitz, T. Reps, and D. Binkley, Interprocedural slicing using dependence graphs, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, PLDI '88, pp.35-46, 1988.
DOI : 10.1145/77606.77608

URL : https://minds.wisconsin.edu/bitstream/handle/1793/58948/TR756.pdf?sequence=1

L. Huang and D. Chiang, Better k-best parsing, Proceedings of the Ninth International Workshop on Parsing Technology, Parsing '05, pp.53-64, 2005.

C. R. Iosif and R. Sisto, Modeling and validation of Java multi-threading applications using Spin, Proceedings of the 4th International SPIN Workshop, 1998.

R. Iosif, M. B. Dwyer, and J. Hatcliff, Translating java for multiple model checkers : The bandera back-end. Formal Methods in System Design, pp.137-180, 1007.

G. Jacob, H. Debar, and E. Filiol, Behavioral detection of malware: from a survey towards an established taxonomy, Journal in Computer Virology, vol.3548, issue.3, pp.251-266, 2008.
DOI : 10.1007/s11416-008-0086-0

G. Jacob, H. Debar, and E. Filiol, Malware Behavioral Detection by Attribute-Automata Using Abstraction from Platform and Language, International Symposium on Recent Advances in Intrusion Detection, pp.81-100, 2009.
DOI : 10.1109/SECPRI.2002.1004372

K. Jiang, Model Checking C Programs by Translating C to Promela, 2009.

D. Neil, S. S. Jones, and . Muchnick, Flow analysis and optimization of lisp-like structures, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, POPL '79, pp.244-256, 1979.

D. Neil, S. S. Jones, and . Muchnick, A flexible approach to interprocedural data flow analysis and programs with recursive data structures, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '82, pp.66-74, 1982.

J. Kinder, S. Katzenbeisser, C. Schallhart, and H. Veith, Detecting Malicious Code by Model Checking, Conference on Detection of Intrusions and Malware & Vulnerability Assessment, pp.174-187, 2005.
DOI : 10.1007/11506881_11

URL : http://wwwbrauer.in.tum.de/~katzenbe/download/mcode.ps.gz

J. Kinder, H. Veith, and F. Zuleger, An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries, Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, pp.214-228, 2009.
DOI : 10.1016/S0167-6423(01)00014-4

E. Kirda, C. Kruegel, G. Banks, G. Vigna, and R. Kemmerer, Behaviorbased Spyware Detection, Proceedings of the 15th USENIX Security Symposium, 2006.

K. Knight and J. May, Applications of Weighted Automata in Natural Language Processing, Handbook of Weighted Automata Theoretical Computer Science. An EATCS Series, pp.571-596, 2009.
DOI : 10.1007/978-3-642-01492-5_14

C. Kolbitsch, P. M. Comparetti, C. Kruegel, E. Kirda, X. Zhou et al., Effective and efficient malware detection at the end host, Proceedings of the 18th conference on USENIX security symposium, SSYM'09, pp.351-366, 2009.

F. Kröger and S. Merz, Temporal Logic and State Systems. Texts in Theoretical Computer Science. An EATCS Series, 2008.

W. Kuich, Tree transducers and formal tree series, Acta Cybern, pp.135-164, 1999.

W. Kuich and A. Salomaa, Semirings, Automata and Languages, 1985.
DOI : 10.1007/978-3-642-69959-7

W. Landi and B. G. Ryder, Pointer-induced aliasing: a problem taxonomy, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.93-103, 1991.
DOI : 10.1145/99583.99599

A. Baudouin-le-charlier, M. Mounji, and . Swimmer, Dynamic detection and classification of computer viruses using general behaviour patterns, International Virus Bulletin Conference, pp.1-22, 1995.

. Mandiant, M-trends 2010 -the advanced persistent threat, 2010.

L. Martignoni, E. Stinson, M. Fredrikson, S. Jha, and J. C. Mitchell, A Layered Architecture for Detecting Malicious Behaviors, International symposium on Recent Advances in Intrusion Detection, pp.78-97, 2008.
DOI : 10.1007/978-3-540-87403-4_5

R. Mateescu and D. Thivolle, A Model Checking Language for Concurrent Value-Passing Systems, World Congress on Formal Methods, pp.148-164, 2008.
DOI : 10.1007/978-3-540-68237-0_12

URL : https://hal.archives-ouvertes.fr/inria-00315312

J. May, K. Knight, and H. Vogler, Efficient inference through cascades of weighted tree transducers, Proceedings of the 48th Annual Meeting of the Association for Computational Linguistics, ACL '10, pp.1058-1066, 2010.

K. Mcmillan, Lazy Annotation for Program Testing and Verification, Computer Aided Verification, pp.104-118, 2010.
DOI : 10.1007/978-3-642-14295-6_10

M. Mohri, Finite-state transducers in language and speech processing, Comput. Linguist, vol.23, pp.269-311, 1997.

M. Mohri, Statistical natural language processing, Applied Combinatorics on Words, 2005.

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

Y. Park, D. Reeves, V. Mulukutla, and B. Sundaravel, Fast malware classification by automated behavioral graph matching, Proceedings of the Sixth Annual Workshop on Cyber Security and Information Intelligence Research, CSIIRW '10, pp.1-45, 2010.
DOI : 10.1145/1852666.1852716

D. Quist and . Valsmith, Covert debugging circumventing software armoring techniques, Blackhat Briefings, 2007.

C. William and . Rounds, Mappings and grammars on trees, Theory of Computing Systems, pp.257-287, 1970.

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

B. G. Ryder, W. A. Landi, P. A. Stocks, S. Zhang, and R. Altucher, A schema for interprocedural modification side-effect analysis with pointer aliasing, ACM Trans. Program. Lang. Syst, vol.23, pp.105-186, 2001.

M. Sagiv, T. Reps, and R. Wilhelm, Solving shapeanalysis problems in languages with destructive updating, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '96, pp.16-31, 1996.

R. Sekar, M. Bendre, D. Dhurjati, and P. Bollineni, A fast automatonbased method for detecting anomalous program behaviors, IEEE Symposium on Security and Privacy Menaces sur les systèmes informatiques, pp.144-155, 2001.

A. Muazzam and . Siddiqui, Data mining methods for malware detection, p.3335368, 2008.

K. Prabhat, A. Singh, and . Lakhotia, Static verification of worm and virus behavior in binary executables using model checking, Information Assurance Workshop, pp.298-300, 2003.

J. W. Thatcher, Generalized2 sequential machine maps, Journal of Computer and System Sciences, vol.4, issue.4, pp.339-367, 1970.
DOI : 10.1016/S0022-0000(70)80017-4

URL : https://doi.org/10.1016/s0022-0000(70)80017-4

S. Thompson, A survey on model checking java programs, 1999.

F. Laurentiu, T. , and E. Mäkinen, On the complexity of a problem on monadic string rewriting systems, Journal of Automata, Languages and Combinatorics, vol.7, issue.4, pp.599-609, 2002.

G. Vigna, Static Disassembly and Code Analysis, Malware Detection of Advances in Information Security, pp.19-41, 2007.
DOI : 10.1007/978-0-387-44599-1_2