Secrecy by typing in security protocols, Journal of the ACM, vol.46, issue.5, pp.749-786, 1999. ,
Implementation of the dataflow synchronous language Signal, Conference on Programming Language Design and Implementation (PLDI'95), pp.163-173, 1995. ,
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 formal approach to large SOFTWARE CONSTRUCTION, Mathematics of Program Construction (MPC), pp.1-20, 1989. ,
DOI : 10.1007/3-540-51305-1_1
Cache behavior prediction by abstract interpretation, 3rd Static Analysis Symposium (SAS'96), pp.51-66, 1996. ,
DOI : 10.1007/3-540-61739-6_33
Improving data-flow analysis with path profiles, Conference on Programming Languages, Design and Implementation (PLDI'98), pp.72-84, 1998. ,
Modern Compiler Implementation in ML, 1999. ,
Foundational Proof-Carrying Code, 16th Symposium on Logics in Computer Science (LICS'2001), pp.247-256, 2001. ,
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. ,
A Static Analyzer for Large Safety Critical Software, Conference on Programming Languages, Design and Implementation (PLDI'03), pp.196-207, 2003. ,
A certified compiler for an imperative language, 1998. ,
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
Compiler transformations for high-performance computing, ACM Computing Surveys, vol.26, issue.4, pp.345-420, 1994. ,
DOI : 10.1145/197405.197406
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. ,
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
Automatic predicate abstraction of c programs, Conference on Programming Languages , Design and Implementation (PLDI'01), pp.203-213, 2001. ,
From symptom to cause: localizing errors in counterexample traces, 30th Symposium on Principles of Programming Languages (POPL'03), pp.97-105, 2003. ,
Abstract interpretation by dynamic partitioning, Journal of Functional Programming, vol.2, issue.4, pp.407-423, 1992. ,
Efficient chaotic iteration strategies with widenings, International Conference on Formal Methods in Programming and their Applications, pp.128-142, 1993. ,
Automatically validating temporal safety properties of interfaces, 8th International SPIN Workshop, pp.103-122, 2001. ,
DOI : 10.1007/3-540-45139-0_7
The slam project: debugging system software via static analysis, 29th Symposium on Principles of Programming Languages (POPL'02), pp.1-3, 2002. ,
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
Graph based algorithms for boolean function manipulation, IEEE Transactions on Computers, issue.35, pp.677-691, 1986. ,
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
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. ,
Abstract interpretation frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992. ,
Systematic design of program transformation frameworks by abstract interpretation, 29th Symposium on Principles of Programming Languages (POPL'02), pp.178-190, 2002. ,
The ASTRÉEASTR´ASTRÉE analyzer, European Symposium On Programming (ESOP'05), pp.21-30, 2005. ,
Conditioned program slicing. Information and Software Technology, pp.595-608, 1998. ,
The Semantics of Program dependence, Conference on Programming Languages, Design and Implementation (PLDI'89), pp.13-27, 1989. ,
Counterexampleguided abstraction refinement, 12th Conference on Computer Aided Verification, pp.154-169, 2000. ,
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
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
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
Semantics-based Program Analysis via Symbolic Composition of Transfer Relations, 1996. ,
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. ,
Semantic foundations of program analysis, Program Flow Analysis: Theory and Applications, pp.303-342, 1981. ,
Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Electronic Notes in Theoretical Computer Science, vol.6, 1997. ,
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
Certification of programs for secure information flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977. ,
DOI : 10.1145/359636.359712
A lattice model of secure information flow, Communications of the ACM, vol.19, issue.5, pp.236-243, 1976. ,
Interprocedural may-alias analysis for pointers: beyond klimiting, Conference on Programming Languages, Design and Implementation (PLDI'94), pp.230-241, 1994. ,
Guarded commands and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975. ,
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. ,
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
Model-Checking Generating counter examples for sound abstract interpretation, 2002. ,
ConSIT: a fully automated conditioned program slicer. Software -Practice and Experience, pp.15-46, 2004. ,
The arithmetic-geometric progression abstract domain, 6th conference on Verification, Model-Cecking and Abstract Interpretation (VM- CAI'05), pp.2-18, 2004. ,
Static analysis of digital filters, European Symposium On Programming number 2986, 2004. ,
Extended static checking for java, Conference on Programming Languages, Design and Implementation (PLDI'02), pp.234-245, 2002. ,
Applying Compiler Techniques to Cache Behavior Prediction, Workshop on Languages, Compilers and Tools for Real-Time Systems (LCT-RTS), pp.37-46, 1997. ,
Automatic state reaching for debugging reactive programs, 5th International Workshop on Automated Debugging (AADEBUG'03), 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-00000840
Security Policies and Security Models, 1982 IEEE Symposium on Security and Privacy, 1982. ,
DOI : 10.1109/SP.1982.10014
Non-standard semantics for program slicing. Higher-Order and Symbolic Computation (HOSC), pp.297-339, 2003. ,
Abstract non-interference: parameterizing non-interference by abstract interpretation, 31st Symposium on Principles of Programming Languages, pp.186-197, 2004. ,
Region-based memory management in Cyclone, Conference on Programming Languages, Design and Implementation (PLDI'02), pp.282-293, 2002. ,
Static analysis of arithmetical congruences, In International Journal of Computer Mathematics, vol.30, pp.165-190, 1989. ,
Improving the results of static analyses programs by local decreasing iteration, Foundations of Software Technology and Theoretical Computer Science (FSTTCS'92), pp.68-79 ,
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
A framework for numeric analysis of array operations, 32nd Symposium on Principles of Programming Languages (POPL'05), pp.338-350, 2005. ,
The synchronous dataflow programming language Lustre, Proceedings of the IEEE, pp.1305-1320, 1991. ,
The next 700 slicing criteria, 2nd UK workshop on program comprehension, 1996. ,
An efficient general iterative algorithm for dataflow analysis, Acta Informatica, vol.24, issue.6, pp.679-694, 1987. ,
DOI : 10.1007/BF00282621
Conditioned slicing supports partition testing, Journal of Software Testing, Verification and Reliability, vol.12, issue.1, pp.23-28, 2002. ,
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. ,
Qualified Data Flow Problems, 7th Symposium on Principles of Programming Languages (POPL'80), pp.68-82, 1980. ,
DOI : 10.1109/TSE.1981.234509
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
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
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
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. ,
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
Path slicing, Conference on Programming Languages , Design and Implementation (PLDI'05), pp.38-47, 2005. ,
DOI : 10.1145/1065010.1065016
Affine relationships among variables of a program, Acta Informatica, vol.6, pp.133-151, 1976. ,
A unified approach to global program optimization, 1st Symposium on Principles of Programming Languages (POPL'73), pp.194-206, 1973. ,
Dynamic program slicing, Information Processing Letters, vol.29, issue.3, pp.155-163, 1988. ,
DOI : 10.1016/0020-0190(88)90054-3
The Art of Computer Programming, 1962. ,
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
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. ,
The Java(tm) Virtual Machine Specification, 2005. ,
Representation of Sets of Trees for Abstract Interpretation, 1999. ,
Tree schemata and fair termination, 7th Static Analyis Symposium (SAS'00), volume 1824 of LNCS, pp.302-320, 2000. ,
TALx86: A Realistic Typed Assembly Language, ACM SIGPLAN Workshop on Compiler Support for System Software, pp.25-35, 1999. ,
The Octagon Abstract Domain, WCRE), pp.310-319, 2001. ,
Relational abstract domains for the detection of floating-point runtime errors, European Symposium On Programming, pp.3-17, 2004. ,
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. ,
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
Co-induction in relational semantics, Theoretical Computer Science, vol.87, issue.1, pp.209-220, 1991. ,
DOI : 10.1016/0304-3975(91)90033-X
The TIL/ML Compiler: Performance and Safety Through Types, ACM SIGPLAN Workshop on Compiler Support for Systems Software, 1996. ,
Proof-Carrying Code, 24th Symposium on Principles of Programming Langauges (POPL '97), pp.106-119, 1997. ,
Translation Validation for an Optimizing Compiler, Conference on Programming Language Design and Implementation (PLDI'00), pp.83-94, 2000. ,
The Design and Implementation of a Certifying Compiler, Conference on Programming Languages, Design and Implementation (PLDI'98), pp.162-173, 1998. ,
Ccured: type-safe retrofitting of legacy code, 29th Symposium on Principles of Programming Languages (POPL'02), pp.128-139, 2002. ,
The objective caml system ,
On context-free languages, Journal of the ACM, vol.13, issue.4, pp.570-581, 1966. ,
Isabelle: A Generic Theorem Prover, LNCS, vol.828, 1994. ,
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
A structural approach to operational semantics, 1981. ,
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
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
Understanding the origin of alarms in astrée, 12th Static Analysis Symposium (SAS'05), pp.303-319, 2005. ,
Outline of a mathematical theory of computation, 1970. ,
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
Two approaches to interprocedural data flow analysis, Program Flow Analysis: Theory and Applications, pp.189-233, 1981. ,
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 lattice theoretical fixpoint theorem and its application, Pacific Journal of Mathematics, vol.5, pp.285-310, 1955. ,
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. ,
Fast and Precise WCET Prediction by Seperate Cache and Path Analyses. Real-Time Systems, 2000. ,
Key Instructions: Solving the Code Location Problem for Optimized Code, Research Report, vol.164, 2000. ,
A Practical, Robust Method for Generating Variable Range Tables, Research Report, vol.165, 2000. ,
A survey of program slicing techniques, Journal of Programming Languages, vol.3, issue.3, 1995. ,
TIL: A Type-Directed Optimizing Compiler for ML, Conference on Programming Language Design and Implementation (PLDI'96), pp.181-192, 1996. ,
Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs, 3rd Static Analysis Symposium (SAS'96), 1996. ,
Program slicing, 5th International Conference on Software Engineering, pp.439-449, 1981. ,
Modular elliptic curves and Fermat's last Theorem, Annals of Mathematics, 1995. ,
Compiler Design, 1994. ,
DOI : 10.1007/978-3-642-17540-4
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
Translation Run-Time Validation of Optimized Code, In Electronic Notes in Theoretical Computer Science, vol.65, 2002. ,
VOC, Electronic Notes in Theoretical Computer Science, 2002. ,
DOI : 10.1016/S1571-0661(04)80393-1
44 3.5 Semantics defined with symbolic transfer functions, p.51 ,
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 ,