]. M. Bibliography-[-aba99 and . Abadi, Secrecy by typing in security protocols, Journal of the ACM, vol.46, issue.5, pp.749-786, 1999.

L. [. Amagbégnon, P. L. Besnard, and . Guernic, Implementation of the dataflow synchronous language Signal, Conference on Programming Language Design and Implementation (PLDI'95), pp.163-173, 1995.

M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.147-160, 1999.
DOI : 10.1145/292540.292555

A. Abrial, A formal approach to large SOFTWARE CONSTRUCTION, Mathematics of Program Construction (MPC), pp.1-20, 1989.
DOI : 10.1007/3-540-51305-1_1

M. Alt, C. Ferdinand, F. Martin, and R. Wilhelm, Cache behavior prediction by abstract interpretation, 3rd Static Analysis Symposium (SAS'96), pp.51-66, 1996.
DOI : 10.1007/3-540-61739-6_33

J. [. Ammons and . Larus, Improving data-flow analysis with path profiles, Conference on Programming Languages, Design and Implementation (PLDI'98), pp.72-84, 1998.

]. A. App99 and . Appel, Modern Compiler Implementation in ML, 1999.

]. A. App01 and . Appel, Foundational Proof-Carrying Code, 16th Symposium on Logics in Computer Science (LICS'2001), pp.247-256, 2001.

]. B. Bcc-+-02, P. Blanchet, R. Cousot, J. Cousot, L. Feret et al., Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter, The Essence of Computation: Complexity, pp.85-108, 2002.

]. B. Bcc-+-03a, P. Blanchet, R. Cousot, J. Cousot, L. Feret et al., A Static Analyzer for Large Safety Critical Software, Conference on Programming Languages, Design and Implementation (PLDI'03), pp.196-207, 2003.

]. Y. Ber98 and . Bertot, A certified compiler for an imperative language, 1998.

G. [. Berry and . Gonthier, The Esterel synchronous programming language: design, semantics, implementation, Science of Computer Programming, vol.19, issue.2, pp.87-152, 1992.
DOI : 10.1016/0167-6423(92)90005-V

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

S. [. Bacon, O. J. Graham, and . Sharp, Compiler transformations for high-performance computing, ACM Computing Surveys, vol.26, issue.4, pp.345-420, 1994.
DOI : 10.1145/197405.197406

R. [. Bodík, M. L. Gupta, and . Soffa, Refining data flow information using infeasible paths, 6th European Software Engineering Conference and 5th ACM SIGSOFT Symposium on Foundations of Software Engineering, pp.361-377, 1997.

J. [. Ball and . Larus, Efficient path profiling, Proceedings of the 29th Annual IEEE/ACM International Symposium on Microarchitecture. MICRO 29, pp.46-57, 1996.
DOI : 10.1109/MICRO.1996.566449

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.138.7451

R. [. Ball, T. D. Majumdar, S. K. Millstein, and . Rajamani, Automatic predicate abstraction of c programs, Conference on Programming Languages , Design and Implementation (PLDI'01), pp.203-213, 2001.

M. [. Ball, S. K. Naik, and . Rajamani, From symptom to cause: localizing errors in counterexample traces, 30th Symposium on Principles of Programming Languages (POPL'03), pp.97-105, 2003.

]. F. Bou92 and . Bourdoncle, Abstract interpretation by dynamic partitioning, Journal of Functional Programming, vol.2, issue.4, pp.407-423, 1992.

]. F. Bou93 and . Bourdoncle, Efficient chaotic iteration strategies with widenings, International Conference on Formal Methods in Programming and their Applications, pp.128-142, 1993.

S. [. Ball and . Rajamani, Automatically validating temporal safety properties of interfaces, 8th International SPIN Workshop, pp.103-122, 2001.
DOI : 10.1007/3-540-45139-0_7

S. [. Ball and . Rajamani, The slam project: debugging system software via static analysis, 29th Symposium on Principles of Programming Languages (POPL'02), pp.1-3, 2002.

T. [. Balakrishnan and . Reps, Analyzing Memory Accesses in x86 Executables, 13th International Conference on Compiler Construction, pp.5-23, 2004.
DOI : 10.1007/978-3-540-24723-4_2

]. R. Bry86 and . Bryant, Graph based algorithms for boolean function manipulation, IEEE Transactions on Computers, issue.35, pp.677-691, 1986.

M. [. Choi, P. Burke, and . Carini, Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.232-245, 1993.
DOI : 10.1145/158511.158639

R. [. Cousot, . Cousotcc79-]-p, R. Cousot, R. Cousot, and . Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints Systematic design of program analysis frameworks Abstract interpretation and application to logic programs, 4th Symposium on Principles of Programming Languages (POPL'77) 6th Symposium on Principles of Programming Languages (POPL'79), pp.238-252, 1977.

]. P. Cc92b, R. Cousot, and . Cousot, Abstract interpretation frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.

R. [. Cousot and . Cousot, Systematic design of program transformation frameworks by abstract interpretation, 29th Symposium on Principles of Programming Languages (POPL'02), pp.178-190, 2002.

. Ccf-+-05-]-p, R. Cousot, J. Cousot, L. Feret, A. Mauborgne et al., The ASTRÉEASTR´ASTRÉE analyzer, European Symposium On Programming (ESOP'05), pp.21-30, 2005.

A. [. Canfora, A. Cimitile, and . Lucia, Conditioned program slicing. Information and Software Technology, pp.595-608, 1998.

M. [. Cartwright and . Felleisen, The Semantics of Program dependence, Conference on Programming Languages, Design and Implementation (PLDI'89), pp.13-27, 1989.

. M. Cgj-+-00-]-e, O. Clarke, S. Grumberg, Y. Jha, H. Lu et al., Counterexampleguided abstraction refinement, 12th Conference on Computer Aided Verification, pp.154-169, 2000.

N. [. Cousot and . Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-97, 1978.
DOI : 10.1145/512760.512770

P. [. Colby and . Lee, Trace-based program analysis, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.195-207, 1996.
DOI : 10.1145/237721.237776

[. Chang and R. Leino, Abstract Interpretation with Alien Expressions and Heap Structures, 4th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), pp.147-163, 2005.
DOI : 10.1007/978-3-540-30579-8_11

]. C. Col96 and . Colby, Semantics-based Program Analysis via Symbolic Composition of Transfer Relations, 1996.

]. P. Cou78 and . Cousot, Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes, 1978.

]. P. Cou81 and . Cousot, Semantic foundations of program analysis, Program Flow Analysis: Theory and Applications, pp.303-342, 1981.

]. P. Cou97a and . Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Electronic Notes in Theoretical Computer Science, vol.6, 1997.

P. Cousot, Types as abstract interpretations, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.316-331, 1997.
DOI : 10.1145/263699.263744

P. [. Denning and . Denning, Certification of programs for secure information flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977.
DOI : 10.1145/359636.359712

]. D. Den76 and . Denning, A lattice model of secure information flow, Communications of the ACM, vol.19, issue.5, pp.236-243, 1976.

]. A. Deu94 and . Deutsch, Interprocedural may-alias analysis for pointers: beyond klimiting, Conference on Programming Languages, Design and Implementation (PLDI'94), pp.230-241, 1994.

]. E. Dji75 and . Djikstra, Guarded commands and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.

S. [. Das, M. Lerner, and . Seigle, Esp: Path-sensitive program verification in polynomial time CSSV: Towards a realistic tool for statically detecting all buffer overflows in C, Conference on Programming Languages, Design and Implementation (PLDI'02) BIBLIOGRAPHY [DRS03] N. Dor, M. Rodeh, and M. Sagiv Conference on Programming Languages, Design and Implementation (PLDI'03), pp.57-68, 2002.

S. [. Déharbe, E. M. Shankar, and . Clarke, Model Checking VHDL with CV, Formal Methods in Computer-Aided Design (FMCAD'98), pp.508-514, 1998.
DOI : 10.1007/3-540-49519-3_33

O. Grumberg, E. M. Clarke, and D. Peled, Model-Checking Generating counter examples for sound abstract interpretation, 2002.

S. [. Fox, M. Danicic, R. M. Harman, and . Hierons, ConSIT: a fully automated conditioned program slicer. Software -Practice and Experience, pp.15-46, 2004.

]. J. Fer04a and . Feret, The arithmetic-geometric progression abstract domain, 6th conference on Verification, Model-Cecking and Abstract Interpretation (VM- CAI'05), pp.2-18, 2004.

]. J. Fer04b and . Feret, Static analysis of digital filters, European Symposium On Programming number 2986, 2004.

C. Flanagan, K. R. Leino, M. Lillibridge, G. Nelson, J. B. Saxe et al., Extended static checking for java, Conference on Programming Languages, Design and Implementation (PLDI'02), pp.234-245, 2002.

C. Ferdinand, F. Martin, and R. Wilhelm, Applying Compiler Techniques to Cache Behavior Prediction, Workshop on Languages, Compilers and Tools for Real-Time Systems (LCT-RTS), pp.37-46, 1997.

E. [. Gaucher, B. Jahier, F. Jeannet, and . Maraninchi, Automatic state reaching for debugging reactive programs, 5th International Workshop on Automated Debugging (AADEBUG'03), 2003.
URL : https://hal.archives-ouvertes.fr/hal-00000840

J. [. Goguen and . Meseguer, Security Policies and Security Models, 1982 IEEE Symposium on Security and Privacy, 1982.
DOI : 10.1109/SP.1982.10014

I. [. Giacobazzi and . Mastroeni, Non-standard semantics for program slicing. Higher-Order and Symbolic Computation (HOSC), pp.297-339, 2003.

I. [. Giacobazzi and . Mastroeni, Abstract non-interference: parameterizing non-interference by abstract interpretation, 31st Symposium on Principles of Programming Languages, pp.186-197, 2004.

]. D. Gmj-+-02, J. G. Grossman, T. Morrisett, M. W. Jim, Y. Hicks et al., Region-based memory management in Cyclone, Conference on Programming Languages, Design and Implementation (PLDI'02), pp.282-293, 2002.

]. P. Gra89 and . Granger, Static analysis of arithmetical congruences, In International Journal of Computer Mathematics, vol.30, pp.165-190, 1989.

]. P. Gra92 and . Granger, Improving the results of static analyses programs by local decreasing iteration, Foundations of Software Technology and Theoretical Computer Science (FSTTCS'92), pp.68-79

F. [. Giacobazzi, F. Ranzato, and . Scozzari, Making abstract interpretations complete, Journal of the ACM, vol.47, issue.2, pp.361-416, 2000.
DOI : 10.1145/333979.333989

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.2353

T. [. Gopan, M. Reps, and . Sagiv, A framework for numeric analysis of array operations, 32nd Symposium on Principles of Programming Languages (POPL'05), pp.338-350, 2005.

P. [. Halbwachs, P. Caspi, D. Raymond, and . Pilaud, The synchronous dataflow programming language Lustre, Proceedings of the IEEE, pp.1305-1320, 1991.

M. Harman, S. Danicic, Y. Sivagurunathan, and D. Simpson, The next 700 slicing criteria, 2nd UK workshop on program comprehension, 1996.

A. [. Horwitz, T. Demers, and . Teitelbaum, An efficient general iterative algorithm for dataflow analysis, Acta Informatica, vol.24, issue.6, pp.679-694, 1987.
DOI : 10.1007/BF00282621

. M. Hhf-+-02-]-r, M. Hierons, C. Harman, L. Fox, M. Ouarbya et al., Conditioned slicing supports partition testing, Journal of Software Testing, Verification and Reliability, vol.12, issue.1, pp.23-28, 2002.

H. N. Halbwachs, F. Lagnier, and P. Raymond, Traces Abstraction in Static Analysis and Program Transformation Xavier Rival BIBLIOGRAPHY Synchronous observers and the verification of reactive systems, Algebraic Methodology and Software Technology (AMAST '93), Workshops in Computing, pp.83-96, 1993.

B. [. Holley and . Rosen, Qualified Data Flow Problems, 7th Symposium on Principles of Programming Languages (POPL'80), pp.68-82, 1980.
DOI : 10.1109/TSE.1981.234509

T. [. Horwitz, D. Reps, and . Binkley, Interprocedural slicing using dependence graphs, Conference on Programming Languages, Design and Implementation (PLDI'88), pp.35-46, 1988.
DOI : 10.1145/989393.989419

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4405

T. [. Horwitz, D. Reps, and . Binkley, Interprocedural slicing using dependence graphs, ACM Transactions on Programming Languages and Systems, vol.12, issue.1, pp.26-60, 1990.
DOI : 10.1145/77606.77608

S. [. Handjieva and . Tzolovski, Refining Static Analyses by Trace-Based Partitioning Using Control Flow, 5th International Static Analysis Symposium (SAS'98), volume 1503 of LNCS, pp.200-214, 1998.
DOI : 10.1007/3-540-49727-7_12

]. B. Jea03 and . Jeannet, Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems, Formal Methods in System Design, vol.23, issue.1, pp.5-37, 2003.

N. [. Jeannet, P. Halbwachs, and . Raymond, Dynamic Partitioning in Analyses of Numerical Properties, 6th Static Analysis Symposium (SAS'99), pp.39-50, 1999.
DOI : 10.1007/3-540-48294-6_3

R. [. Jhala and . Majumdar, Path slicing, Conference on Programming Languages , Design and Implementation (PLDI'05), pp.38-47, 2005.
DOI : 10.1145/1065010.1065016

]. M. Kar76 and . Karr, Affine relationships among variables of a program, Acta Informatica, vol.6, pp.133-151, 1976.

]. G. Kil73 and . Kildall, A unified approach to global program optimization, 1st Symposium on Principles of Programming Languages (POPL'73), pp.194-206, 1973.

J. [. Korel and . Laski, Dynamic program slicing, Information Processing Letters, vol.29, issue.3, pp.155-163, 1988.
DOI : 10.1016/0020-0190(88)90054-3

]. D. Knu62 and . Knuth, The Art of Computer Programming, 1962.

[. Lev-ami and M. Sagiv, TVLA: A System for Implementing Static Analyses, 7th Static Analysis Symposium (SAS'00), pp.280-301, 2000.
DOI : 10.1007/978-3-540-45099-3_15

]. X. Ler06 and . Leroy, Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant, 33rd Symposium on Principles of Programming Languages (POPL'06), 2006.

F. [. Lindholm and . Yellin, The Java(tm) Virtual Machine Specification, 2005.

]. L. Mau99 and . Mauborgne, Representation of Sets of Trees for Abstract Interpretation, 1999.

]. L. Mau00 and . Mauborgne, Tree schemata and fair termination, 7th Static Analyis Symposium (SAS'00), volume 1824 of LNCS, pp.302-320, 2000.

. Mcg-+-99-]-g, K. Morrisett, N. Crary, D. Glew, R. Grossman et al., TALx86: A Realistic Typed Assembly Language, ACM SIGPLAN Workshop on Compiler Support for System Software, pp.25-35, 1999.

]. A. Min01 and . Miné, The Octagon Abstract Domain, WCRE), pp.310-319, 2001.

]. A. Min04 and . Miné, Relational abstract domains for the detection of floating-point runtime errors, European Symposium On Programming, pp.3-17, 2004.

]. A. Min06 and . Miné, Symbolic methods to enhance the precision of numerical abstract domains, 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'06), pp.348-363, 2006.

T. [. Melski and . Reps, The Interprocedural Express-Lane Transformation, 12th International Conference on Compiler Construction (CC'03), pp.200-216, 2003.
DOI : 10.1007/3-540-36579-6_15

M. [. Milner and . Tofte, Co-induction in relational semantics, Theoretical Computer Science, vol.87, issue.1, pp.209-220, 1991.
DOI : 10.1016/0304-3975(91)90033-X

. Mtc-+-96-]-g, D. Morrisett, P. Tarditi, C. Cheng, R. Stone et al., The TIL/ML Compiler: Performance and Safety Through Types, ACM SIGPLAN Workshop on Compiler Support for Systems Software, 1996.

]. G. Nec97 and . Necula, Proof-Carrying Code, 24th Symposium on Principles of Programming Langauges (POPL '97), pp.106-119, 1997.

]. G. Nec00 and . Necula, Translation Validation for an Optimizing Compiler, Conference on Programming Language Design and Implementation (PLDI'00), pp.83-94, 2000.

P. [. Necula and . Lee, The Design and Implementation of a Certifying Compiler, Conference on Programming Languages, Design and Implementation (PLDI'98), pp.162-173, 1998.

S. [. Necula, W. Mcpeak, and . Weimer, Ccured: type-safe retrofitting of legacy code, 29th Symposium on Principles of Programming Languages (POPL'02), pp.128-139, 2002.

. Oca and . Ocaml, The objective caml system

]. R. Par66 and . Parikh, On context-free languages, Journal of the ACM, vol.13, issue.4, pp.570-581, 1966.

]. L. Pau94 and . Paulson, Isabelle: A Generic Theorem Prover, LNCS, vol.828, 1994.

N. [. Pace, P. Halbwachs, and . Raymond, Counter-example generation in symbolic abstract model-checking. Software and Tools for Technology Transfer (STTT), pp.158-164, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00199168

]. G. Plo81 and . Plotkin, A structural approach to operational semantics, 1981.

O. [. Pnueli, M. Shtrichman, and . Siegel, Translation validation for synchronous languages, 25th International Colloquium on Automata, Languages and Programming (ICALP'98), volume 1443 of LNCS, pp.235-246, 1998.
DOI : 10.1007/BFb0055057

S. [. Reps, M. Horwitz, and . Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '95, pp.49-61, 1995.
DOI : 10.1145/199448.199462

]. X. Riv05b, Understanding the origin of alarms in astrée, 12th Static Analysis Symposium (SAS'05), pp.303-319, 2005.

]. D. Sco70 and . Scott, Outline of a mathematical theory of computation, 1970.

A. [. Sabelfeld and . 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

A. [. Sharir and . Pnuelli, Two approaches to interprocedural data flow analysis, Program Flow Analysis: Theory and Applications, pp.189-233, 1981.

T. [. Sagiv, R. Reps, and . Wilhelm, Parametric shape analysis via 3-valued logic, Conference on Automated Deduction (CADE), volume 2392 of LNCS, pp.217-298, 2002.
DOI : 10.1145/514188.514190

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.3161

]. A. Tar55 and . Tarski, A lattice theoretical fixpoint theorem and its application, Pacific Journal of Mathematics, vol.5, pp.285-310, 1955.

C. [. Theiling and . Ferdinand, Software Considerations in Airborne Systems and Equipment Certification Combining Abstract Interpretation and ILP for Microarchitecture Modelling and Program Path Analysis, 19th IEEE Real-Time Systems Symposium, pp.144-153, 1998.

H. Theiling, C. Ferdinand, and R. Wilhelm, Fast and Precise WCET Prediction by Seperate Cache and Path Analyses. Real-Time Systems, 2000.

]. C. Tg00a, S. L. Tice, and . Graham, Key Instructions: Solving the Code Location Problem for Optimized Code, Research Report, vol.164, 2000.

]. C. Tg00b, S. L. Tice, and . Graham, A Practical, Robust Method for Generating Variable Range Tables, Research Report, vol.165, 2000.

]. F. Tip95 and . Tip, A survey of program slicing techniques, Journal of Programming Languages, vol.3, issue.3, 1995.

]. D. Tmc-+-96, G. Tarditi, P. Morrisett, C. Cheng, R. Stone et al., TIL: A Type-Directed Optimizing Compiler for ML, Conference on Programming Language Design and Implementation (PLDI'96), pp.181-192, 1996.

]. A. Ven96 and . Venet, Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs, 3rd Static Analysis Symposium (SAS'96), 1996.

]. M. Wei81 and . Weiser, Program slicing, 5th International Conference on Software Engineering, pp.439-449, 1981.

]. A. Wil95 and . Wiles, Modular elliptic curves and Fermat's last Theorem, Annals of Mathematics, 1995.

D. [. Wilhelm and . Maurer, Compiler Design, 1994.
DOI : 10.1007/978-3-642-17540-4

R. [. Xi and . Harper, A dependently typed assembly language, International Conference on Functional Programming, pp.169-180, 2001.
DOI : 10.1145/507635.507657

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.123.266

. Zpf-+-02-]-l, A. Zuck, Y. Pnueli, B. Fang, Y. Goldberg et al., Translation Run-Time Validation of Optimized Code, In Electronic Notes in Theoretical Computer Science, vol.65, 2002.

L. Zuck, A. Pnueli, Y. Fang, and B. Goldberg, VOC, Electronic Notes in Theoretical Computer Science, 2002.
DOI : 10.1016/S1571-0661(04)80393-1

.. Grammar-of-symbolic-transfer-functions, 44 3.5 Semantics defined with symbolic transfer functions, p.51

O. Non-monotonicity, 37 3.2.2 Path semantics 39 3.4.1 Constant propagation and dead code elimination 51 3.4.2 Constant propagation and variable removal 53 3.4.4 Constant propagation and dead code elimination 67 4.3.1 The ordering over the basis 73 4.3.2 Denotational style abstraction of a if -statement 83 5.2.1 Transfer functions in a partitioning analysis 98 5.3.1 Application to the partitioning of an if -statement 101 6.1.1 Infinite loop, with cnt-statement 114 6.2.2 Abstract initial token and push operation, Semantic slicing based on the final state . . . . . . . . . . . . . . . 136 7.2.2 Criterion for the specification of execution patterns . . . . . . . . . 137 7.2.3 Input constraints and errors . . . . . . . . . . . . . . . . . . . . . . 138 7.2.4 Combination of semantic slicing criteria, p.151