?. Wp, ?) = ?, ?? WP(c1, ?2) = ?1, ?1 WP(c2, ?) = ?2, ?2 WP(c1; c2, ?) = ?1, ?? WP(c1, ?) = ?1, ?1 WP(c2, ?) = ?2, pp.2-3

E. Albert, G. Puebla, and M. V. Hermenegildo, Abstraction-Carrying Code, Logic for Programming Artificial Intelligence and Reasoning, number 3452 in Lecture Notes in Computer Science, pp.380-397, 2005.
DOI : 10.1007/978-3-540-32275-7_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.80.9777

B. Alpern, L. Carter, and J. Ferrante, Modeling parallel computers as memory hierarchies, Proceedings of Workshop on Programming Models for Massively Parallel Computers, 1993.
DOI : 10.1109/PMMP.1993.315548

F. Y. Bannwart and P. Müller, A Program Logic for Bytecode, Electronic Notes in Theoretical Computer Science, vol.141, issue.1, pp.255-273, 2005.
DOI : 10.1016/j.entcs.2005.02.026

M. Barnett, B. E. Chang, R. Deline, B. Jacobs, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Formal Methods for Components and Objects, 2005.
DOI : 10.1007/11804192_17

M. Barnett, K. R. Leino, and W. Schulte, The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure and Interoperable Smart Devices: Proceedings of the International Workshop CASSIS, pp.151-171, 2004.
DOI : 10.1007/978-3-540-30569-9_3

C. W. Barrett, Y. Fang, B. Goldberg, Y. Hu, A. Pnueli et al., TVOC: A Translation Validator for Optimizing Compilers, CAV, number 3576 in Lecture Notes in Computer Science, pp.291-295, 2005.
DOI : 10.1007/11513988_29

G. Barthe, B. Grégoire, C. Kunz, and T. Rezk, Certificate translation for optimizing compilers, Static Analysis Symposium, number 4134 in Lecture Notes in Computer Science, pp.301-317, 2006.
DOI : 10.1145/1538917.1538919

G. Barthe, B. Grégoire, and M. Pavlova, Preservation of proof obligations for Java, International Joint Conference on Automated Reasoning, 2008.

G. Barthe and C. Kunz, Certificate translation for specification-preserving advices, Proceedings of the 7th workshop on Foundations of aspect-oriented languages, FOAL '08, pp.9-18, 2008.
DOI : 10.1145/1394496.1394498

G. Barthe and C. Kunz, Certificate??Translation??in??Abstract??Interpretation, European Symposium on Programming, number 4960 in Lecture Notes in Computer Science, pp.368-382, 2008.
DOI : 10.1007/978-3-540-78739-6_28

G. Barthe, C. Kunz, D. Pichardie, and J. Samborski-forlese, Preservation of proof obligations for hybrid verification methods, Software Engineering and Formal Methods, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00332718

G. Barthe, C. Kunz, and J. Sacchini, Certified Reasoning in Memory Hierarchies, Asian Programming Languages and Systems Symposium, Lecture Notes in Computer Science, 2008.
DOI : 10.1007/BF00268134

G. Barthe, D. Naumann, and T. Rezk, Deriving an information flow checker and certifying compiler for Java, 2006 IEEE Symposium on Security and Privacy (S&P'06), 2006.
DOI : 10.1109/SP.2006.13

G. Barthe, T. Rezk, and A. Saabas, Proof Obligations Preserving Compilation, Workshop on Formal Aspects in Security and Trust, number 3866 in Lecture Notes in Computer Science, pp.112-126, 2005.
DOI : 10.1007/11679219_9

G. Barthe, L. Burdy, J. Charles, B. Grégoire, M. Huisman et al., JACK???????A Tool for Validation of Security and Behaviour of Java Applications, Formal Methods for Components and Objects: Revised Lectures from the 5th International Symposium FMCO 2006, number 4709 in Lecture Notes in Computer Science, pp.152-174, 2007.
DOI : 10.1007/978-3-540-74792-5_7

N. Benton, Simple relational correctness proofs for static analyses and program transformations, Principles of Programming Languages, pp.14-25, 2004.

Y. Bertot, B. Grégoire, and X. Leroy, A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis, Lecture Notes in Computer Science, vol.3839, pp.66-81, 2004.
DOI : 10.1007/11617990_5
URL : https://hal.archives-ouvertes.fr/inria-00289549

F. Besson, T. Jensen, and D. Pichardie, Proof-carrying code from certified abstract interpretation and fixpoint compression, Theoretical Computer Science, vol.364, issue.3, pp.273-291, 2006.
DOI : 10.1016/j.tcs.2006.08.012

F. Besson, T. Jensen, D. Pichardie, and T. Turpin, Result certification for relational program analysis, Research Report, vol.6333, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00166930

F. Besson, T. P. Jensen, and T. Turpin, Small Witnesses for Abstract Interpretation-Based Proofs, Programming Languages and Systems: Proceedings of the 16th European Symposium on Programming, ESOP 2007, number 4421 in Lecture Notes in Computer Science, pp.268-283, 2007.
DOI : 10.1007/978-3-540-71316-6_19

S. Blazy, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. R. Kiniry et al., An overview of JML tools and applications, Workshop on Formal Methods for Industrial Critical Systems, pp.73-89, 2003.
DOI : 10.1007/s10009-004-0167-4

L. Burdy and M. Pavlova, Java bytecode specification and verification, Proceedings of the 2006 ACM symposium on Applied computing , SAC '06, pp.1835-1839, 2006.
DOI : 10.1145/1141277.1141708

A. Chaieb, Proof-Producing Program Analysis, Lecture Notes in Computer Science, vol.4281, pp.287-301, 2006.
DOI : 10.1007/11921240_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.3773

P. Chalin, J. R. Kiniry, G. T. Leavens, and E. Poll, Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2, Formal Methods for Components and Objects, pp.342-363, 2006.
DOI : 10.1007/11804192_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.102.4611

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

P. Cousot and R. Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '79, pp.269-282, 1979.
DOI : 10.1145/567752.567778

W. J. Dally, F. Labonte, A. Das, P. Hanrahan, J. Ho-ahn et al., Merrimac, Proceedings of the 2003 ACM/IEEE conference on Supercomputing, SC '03, p.35, 2003.
DOI : 10.1145/1048935.1050187

D. S. Dantas and D. Walker, Harmless advice, Principles of Programming Languages, pp.383-396, 2006.
DOI : 10.1145/1111037.1111071

K. Fatahalian, D. R. Horn, T. J. Knight, L. Leem, M. Houston et al., Sequoia: Programming the Memory Hierarchy, ACM/IEEE SC 2006 Conference (SC'06), p.83, 2006.
DOI : 10.1109/SC.2006.55

C. Flanagan, K. R. Leino, M. Lillibridge, G. Nelson, J. B. Saxe et al., Extended static checking for Java, Programming Languages Design and Implementation, pp.234-245, 2002.

J. D. Guttman and M. Wand, Special issue on VLISP, Lisp and Symbolic Computation, 1995.

N. Halbwachs and M. Péron, Discovering properties about arrays in simple programs, PLDI, pp.339-348, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00288274

M. V. Hermenegildo and F. Rossi, Strict and nonstrict independent and-parallelism in logic programs: Correctness, efficiency, and compile-time conditions, The Journal of Logic Programming, vol.22, issue.1, pp.1-45, 1995.
DOI : 10.1016/0743-1066(93)00007-F

M. Houston, J. Y. Park, M. Ren, T. Knight, K. Fatahalian et al., A portable runtime interface for multi-level memory hierarchies, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming , PPoPP '08, 2008.
DOI : 10.1145/1345206.1345229

U. J. Kapasi, S. Rixner, W. J. Dally, B. Khailany, J. Ho-ahn et al., Programmable stream processors, Computer, vol.36, issue.8, pp.54-62, 2003.
DOI : 10.1109/MC.2003.1220582
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.112.7599

T. J. Knight, J. Y. Park, M. Ren, M. Houston, M. Erez et al., Compilation for explicitly managed memory hierarchies, Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming , PPoPP '07, pp.226-236, 2007.
DOI : 10.1145/1229428.1229477

S. Krishnamurthi, K. Fisler, and M. Greenberg, Verifying aspect advice modularly, SIGSOFT FSE, pp.137-146, 2004.

P. Laud, T. Uustalu, and V. Vene, Type systems equivalent to data-flow analyses for imperative languages, Theoretical Computer Science, vol.364, issue.3, pp.292-310, 2006.
DOI : 10.1016/j.tcs.2006.08.013

K. Rustan and M. Leino, Specifying and verifying programs in spec#, Ershov Memorial Conference, p.20, 2006.

K. Rustan, M. Leino, and W. Schulte, Exception safety for C#, Proceedings of the Second International Conference on Software Engineering and Formal Methods, 2004. SEFM 2004., pp.218-227, 2004.
DOI : 10.1109/SEFM.2004.1347523

S. Lerner, T. Millstein, E. Rice, and C. Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.364-377, 2005.
DOI : 10.1145/1040305.1040335
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.9525

X. Leroy, Coinductive Big-Step Operational Semantics, Programming Languages and Systems: Proceedings of the 15th European Symposium on Programming, pp.54-68, 2006.
DOI : 10.1006/inco.1994.1093
URL : https://hal.archives-ouvertes.fr/inria-00309010

X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Principles of Programming Languages, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

F. Logozzo and M. Fähndrich, On the Relative Completeness of Bytecode Analysis Versus Source Code Analysis, Lecture Notes in Computer Science, vol.4959, pp.197-212, 2008.
DOI : 10.1007/978-3-540-78791-4_14

C. Marché, C. Paulin-mohring, and X. Urbain, The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML, The Journal of Logic and Algebraic Programming, vol.58, issue.1-2, pp.89-106, 2004.
DOI : 10.1016/j.jlap.2003.07.006

A. Miné, Weakly Relational Numerical Abstract Domains, 2004.

P. Müller and M. Nordio, Proof-transforming compilation of programs with abrupt termination. In SAVCBS '07: Proceedings of the 2007 conference on Specification and verification of component-based systems, pp.39-46, 2007.

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

G. C. Necula and P. Lee, Safe kernel extensions without run-time checking, Operating Systems Design and Implementation, pp.229-243, 1996.
DOI : 10.1145/248155.238781
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.6054

G. C. Necula and P. Lee, The design and implementation of a certifying compiler, Programming Languages Design and Implementation, pp.333-344, 1998.

G. C. Necula, Compiling with Proofs, 1998.

C. George and . Necula, Translation validation for an optimizing compiler, ACM SIGPLAN Notices, vol.35, issue.5, pp.83-94, 2000.

M. Nordio, P. Müller, and B. Meyer, Formalizing proof-transforming compilation of eiffel programs, 2008.

M. Nordio, P. Müller, and B. Meyer, Proof-Transforming Compilation of Eiffel Programs, TOOLS-EUROPE, Lecture Notes in Business and Information Processing, 2008.
DOI : 10.1007/978-3-540-69824-1_18

S. Owicki and D. Gries, An axiomatic proof technique for parallel programs I, Acta Informatica, vol.11, issue.4, pp.319-340, 1975.
DOI : 10.1007/BF00268134

M. Pavlova, Java bytecode verification and its applications Thése de doctorat, spécialité informatique, 2007.

A. Pnueli, E. Singerman, and M. Siegel, Translation validation, Lecture Notes in Computer Science, vol.1384, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

A. Saabas and T. Uustalu, A compositional natural semantics and Hoare logic for low-level languages, Theoretical Computer Science, vol.373, issue.3, pp.273-302, 2007.
DOI : 10.1016/j.tcs.2006.12.020

A. Saabas and T. Uustalu, Type Systems for Optimizing Stack-based Code, Bytecode Semantics, Verification, pp.103-119, 2007.
DOI : 10.1016/j.entcs.2007.02.063

A. Saabas and T. Uustalu, Program and proof optimizations with type systems, The Journal of Logic and Algebraic Programming, vol.77, issue.1-2, pp.131-154, 2008.
DOI : 10.1016/j.jlap.2008.05.007
URL : http://doi.org/10.1016/j.jlap.2008.05.007

S. Seo, H. Yang, and K. Yi, Automatic Construction of Hoare Proofs from Abstract Interpretation Results, Asian Programming Languages and Systems Symposium, pp.230-245, 2003.
DOI : 10.1007/978-3-540-40018-9_16

Z. Shao, V. Trifonov, B. Saha, and N. Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems, vol.27, issue.1, pp.1-45, 2005.
DOI : 10.1145/1053468.1053469

M. Strecker, Formal Verification of a Java Compiler in Isabelle, Conference on Automated Deduction, pp.63-77, 2002.
DOI : 10.1007/3-540-45620-1_5

D. Tarditi, J. G. Morrisett, P. Cheng, C. Stone, R. Harper et al., TIL: A type-directed optimizing compiler for ML, Programming Languages Design and Implementation, pp.181-192, 1996.

J. Tristan and X. Leroy, Formal verification of translation validators, ACM SIGPLAN Notices, vol.43, issue.1, pp.17-27, 2008.
DOI : 10.1145/1328897.1328444
URL : https://hal.archives-ouvertes.fr/tel-00437582

M. Wildmoser, A. Chaieb, and T. Nipkow, Bytecode Analysis for Proof Carrying Code, Electronic Notes in Theoretical Computer Science, vol.141, issue.1, 2005.
DOI : 10.1016/j.entcs.2005.02.040

M. Wildmoser, T. Nipkow, G. Klein, and S. Nanz, Prototyping Proof Carrying Code, Theoretical Computer Science, pp.333-347, 2004.
DOI : 10.1007/1-4020-8141-3_27
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.1542

H. Xi and S. Xia, Towards array bound check elimination in java tm virtual machine language, CASCON '99: Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.14, 1999.

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