A Formally Verified Compiler Back-end

Appel, A.W.: Modern Compiler Implementation in ML. Cambridge University Press, Cambridge (1998) Appel, A.W.: Foundational proof-carrying code. In: Logic in Computer Science 2001, pp. 247–258. IEEE Computer Society Press, Silver Spring (2001) Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007. Lecture Notes in Computer Science, vol. 4732, pp. 5–21. Springer, New York (2007) Barrett, C.W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A, Zuck, L.D.: TVOC: a translation validator for optimizing compilers. In: Computer Aided Verification, 17th International Conference, CAV 2005. Lecture Notes in Computer Science, vol. 3576, pp. 291–295. Springer, New York (2005) Barthe, G., Courtieu, P., Dufay, G., Melo de Sousa, S.: Tool-assisted specification and verification of the JavaCard platform. In: Proceedings of AMAST’02. Lecture Notes in Computer Science, vol. 2422, pp. 41–59. Springer, New York (2002) Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Functional and Logic Programming, 8th Int. Symp. FLOPS 2006. Lecture Notes in Computer Science, vol. 3945, pp. 114–129. Springer, New York (2006) Barthe, G., Grégoire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: Static Analysis, 13th Int. Symp., SAS 2006. Lecture Notes in Computer Science, vol. 4134, pp. 301–317. Springer, New York (2006) Barthe, G., Kunz, C.: Certificate translation in abstract interpretation. In: Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008. Lecture Notes in Computer Science, vol. 4960, pp. 368–382. Springer, New York (2008) Benton, N., Hur, C.-K.: Biorthogonality, step-indexing and compiler correctness. In: International Conference on Functional Programming 2009, pp. 97–108. ACM, New York (2009) Beringer, L.: Functional elimination of phi-instructions. In: Proc. 5th Workshop on Compiler Optimization Meets Compiler Verification (COCV 2006). Electronic Notes in Theoretical Computer Science, vol. 176, no. 3, pp. 3–20. Elsevier, Amsterdam (2007) Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development—Coq’Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, New York (2004) Bertot, Y., Grégoire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Types for Proofs and Programs, Workshop TYPES 2004. Lecture Notes in Computer Science, vol. 3839, pp. 66–81. Springer, New York (2006) Bertot, Y., Komendantsky, V.: Fixed point semantics and partial recursion in Coq. In: 10th Int. Conf. on Principles and Practice of Declarative Programming (PPDP 2008), pp. 89–96. ACM, New York (2008) Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.: Putting it all together? Formal verification of the VAMP. Int. J. Softw. Tools Technol. Transf. 8, 411–430 (2006) Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: FM 2006: Int. Symp. on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 460–475. Springer, New York (2006) Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263–288 (2009) Blech, J.O., Glesner, S., Leitner, J., Mülling, S.: Optimizing code generation from SSA form: a comparison between two formal correctness proofs in Isabelle/HOL. In: Proc. COCV Workshop (Compiler Optimization meets Compiler Verification). Electronic Notes in Theoretical Computer Science, vol. 141, no. 2, pp. 33–51. Elsevier, Amsterdam (2005) Boehm, H.-J.: Threads cannot be implemented as a library. In: Programming Language Design and Implementation 2005, pp. 261–268. ACM, New York (2005) Cachera, D., Jensen, T.P., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theor. Comp. Sci. 342(1), 56–78 (2005) Chaitin, G.J.: Register allocation and spilling via graph coloring. In: Symposium on Compiler Construction. SIGPLAN Notices, vol. 17, no. 6, pp. 98–105. ACM, New York (1982) Chen, J., Hawblitzel, C., Perry, F., Emmi, M., Condit, J., Coetzee, D., Pratikaki, P.: Type-preserving compilation for large-scale optimizing object-oriented compilers. In: Programming Language Design and Implementation 2008, pp. 183–192. ACM, New York (2008) Chirica, L., Martin, A.: Toward compiler implementation correctness proofs. ACM Trans. Program. Lang. Syst. 8(2), 185–214 (1986) Chlipala, A.J.: A certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation 2007, pp. 54–65. ACM, New York (2007) Clemmensen, G., Oest, O.: Formal specification and development of an Ada compiler. In: IEEE Conf. on Soft. Engineering, pp. 430–440. IEEE Computer Society Press, Silver Spring (1984) Coq Development Team: The Coq proof assistant. http://coq.inria.fr/ (1989–2009) Coupet-Grimal, S., Delobel, W.: A uniform and certified approach for two static analyses. In: Types for Proofs and Programs, Workshop TYPES 2004. Lecture Notes in Computer Science, vol. 3839, pp. 115–137. Springer, New York (2006) Dargaye, Z.: Vérification formelle d’un compilateur pour langages fonctionnels. Ph.D. thesis, University Paris 7 Denis Diderot (2009) Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28(6), 2 (2003) Dold, A., Gaul, T., Zimmermann, W.: Mechanized verification of compiler backends. In: Int. Workshop on Software Tools for Technology Transfer, STTT 1998. BRICS Notes, vol. NS-98-4, pp. 13–24. University of Aarhus, Aarhus (1998) Dold, A., Vialard, V.: A mechanically verified compiling specification for a Lisp compiler. In: Proc. FST TCS 2001. Lecture Notes in Computer Science, vol. 2245, pp. 144–155. Springer, New York (2001) Eide, E., Regehr, J.: Volatiles are miscompiled, and what to do about it. In: Proceedings of the 8th ACM & IEEE International Conference on Embedded Software, EMSOFT 2008, pp. 255–264. ACM, New York (2008) Ellis, J.R.: Bulldog: a compiler for VLSI architectures. ACM Doctoral Dissertation Awards series. The MIT Press, Cambridge (1986) Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: Int. Workshop on Types in Language Design and Implementation (TLDI’07), pp. 67–78. ACM, New York (2007) Fox, A.C.J.: Formal specification and verification of ARM6. In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003. Lecture Notes in Computer Science, vol. 2758, pp. 25–40. Springer, New York (2003) George, L., Appel, A.W.: Iterated register coalescing. ACM Trans. Program. Lang. Syst. 18(3), 300–324 (1996) Goos, G., Zimmermann, W.: Verification of compilers. In: Correct System Design, Recent Insight and Advances. Lecture Notes in Computer Science, vol. 1710, pp. 201–230. Springer, New York (1999) Grégoire, B.: Compilation des termes de preuves: un (nouveau) mariage entre Coq et OCaml. Ph.D. thesis, University Paris 7 (2003) Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Static Analysis, 11th Int. Symposium, SAS 2004. Lecture Notes in Computer Science, vol. 3148, pp. 212–227. Springer, New York (2004) Guttman, J., Monk, L., Ramsdell, J., Farmer, W., Swarup, V.: The VLISP verified scheme system. LISP Symb. Comput. 8(1–2), 33–110 (1995) Hales, T.C.: Formal proof. Not. Am. Math. Soc. 55(11), 1370–1380 (2008) Hartel, P.H., Moreau, L.A.V.: Formalizing the safety of Java, the Java virtual machine and Java Card. ACM Comput. Surv. 33(4), 517–558 (2001) Henderson, F.: Accurate garbage collection in an uncooperative environment. In: International Symposium on Memory Management 2002. SIGPLAN Notices, vol. 38, no. 2, pp. 150–156. ACM, New York (2003) Hobor, A., Appel, A.W., Zappa Nardelli, F.: Oracle semantics for concurrent separation logic. In: Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008. Lecture Notes in Computer Science, vol. 4960, pp. 353–367. Springer, New York (2008) Huang, Q., Childers, B.R., Soffa, M.L.: Catching and identifying bugs in register allocation. In: Static Analysis, 13th Int. Symp., SAS 2006. Lecture Notes in Computer Science, vol. 4134, pp. 281–300. Springer, New York (2006) Huet, G.P.: The zipper. J. Funct. Program. 7(5), 549–554 (1997) Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Fundamental Approaches to Software Engineering, 3rd Int. Conf. FASE 2000. Lecture Notes in Computer Science, vol. 1783, pp. 284–303. Springer, New York (2000) IBM Corporation: The PowerPC Architecture. Morgan Kaufmann, San Francisco (1994) Kildall, G.A.: A unified approach to global program optimization. In: 1st Symposium Principles of Programming Languages, pp. 194–206. ACM, New York (1973) Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006) Knoop, J., Koschützki, D., Steffen, B.: Basic-block graphs: living dinosaurs? In: Proc. Compiler Construction ’98. Lecture Notes in Computer Science, vol. 1383, pp. 65–79. Springer, New York (1998) Knoop, J., Rüthing, O., Steffen, B.: Optimal code motion: theory and practice. ACM Trans. Program. Lang. Syst. 16(4), 1117–1155 (1994) Lacey, D., Jones, N.D., Van Wyk, E., Frederiksen, C.C.: Proving correctness of compiler optimizations by temporal logic. In: 29th Symposium Principles of Programming Languages, pp. 283–294. ACM, New York (2002) Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: code generation and implementation correctness. In: Int. Conf. on Software Engineering and Formal Methods (SEFM 2005), pp. 2–11. IEEE Computer Society Press, Silver Spring (2005) Leinenbach, D., Petrova, E.: Pervasive compiler verification. In: 3rd Int. Workshop on Systems Software Verification (SSV 2008). Electronic Notes in Theoretical Computer Science, vol. 217, no. 21, pp. 23–40. Elsevier, Amsterdam (2008) Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: 32nd Symposium Principles of Programming Languages, pp. 364–377. ACM, New York (2005) Leroy, X.: Java bytecode verification: algorithms and formalizations. J. Autom. Reason. 30(3–4), 235–269 (2003) Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42–54. ACM, New York (2006) Leroy, X.: The Compcert verified compiler, software and commented proof. http://compcert.inria.fr/ (2009) Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1–31 (2008) Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284–304 (2009) Letouzey, P.: A new extraction for Coq. In: Types for Proofs and Programs, Workshop TYPES 2002. Lecture Notes in Computer Science, vol. 2646, pp. 200–219. Springer, New York (2003) Letouzey, P.: Extraction in Coq: an overview. In: Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008. Lecture Notes in Computer Science, vol. 5028, pp. 359–369. Springer, New York (2008) Li, G., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007. Lecture Notes in Computer Science, vol. 4421, pp. 205–219. Springer, New York (2007) Li, G., Slind, K.: Compilation as rewriting in higher order logic. In: Automated Deduction, CADE-21. Lecture Notes in Computer Science, vol. 4603, pp. 19–34. Springer, New York (2007) Lindig, C.: Random testing of C calling conventions. In: Proceedings of the Sixth International Workshop on Automated Debugging, AADEBUG 2005, pp. 3–12. ACM, New York (2005) McCarthy, J., Painter, J.: Correctness of a compiler for arithmetical expressions. In: Mathematical Aspects of Computer Science. Proc. of Symposia in Applied Mathematics, vol. 19, pp. 33–41. American Mathematical Society, Providence (1967) McKeeman, W.M.: Differential testing for software. Digit. Tech. J. 10(1), 100–107 (1998) Milner, R., Weyhrauch, R.: Proving compiler correctness in a mechanized logic. In: Meltzer, B., Michie, D. (eds.) Proc. 7th Annual Machine Intelligence Workshop. Machine Intelligence, vol. 7, pp. 51–72. Edinburgh University Press, Edinburgh (1972) Moore, J.S.: A mechanically verified language implementation. J. Autom. Reason. 5(4), 461–492 (1989) Moore, J.S.: Piton: a Mechanically Verified Assembly-Language. Kluwer, Dordrecht (1996) Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. J. Funct. Program. 12(1), 43–88 (2002) Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3), 528–569 (1999) Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco (1997) Müller-Olm, M.: Modular Compiler Verification: a Refinement-Algebraic Approach Advocating Stepwise Abstraction. Lecture Notes in Computer Science, vol. 1283. Springer, New York (1997) Necula, G.C.: Proof-carrying code. In: 24th Symposium Principles of Programming Languages, pp. 106–119. ACM, New York (1997) Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation 2000, pp. 83–95. ACM, New York (2000) Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Compiler Construction, 11th International Conference, CC 2002. Lecture Notes in Computer Science, vol. 2304, pp. 213–228. Springer, New York (2002) Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted software. In: 28th Symposium Principles of Programming Languages, pp. 142–154. ACM, New York (2001) O’Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comp. Sci. 375(1–3), 271–307 (2007) Paul, W., et al.: The Verisoft project. http://www.verisoft.de/ (2003–2008) Peyton Jones, S.L., Ramsey, N., Reig, F.: C- -: a portable assembly language that supports garbage collection. In: PPDP’99: International Conference on Principles and Practice of Declarative Programming. Lecture Notes in Computer Science, vol. 1702, pp. 1–28. Springer, New York (1999) Pichardie, D.: Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés. Ph.D. thesis, University Rennes 1 (2005) Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Tools and Algorithms for Construction and Analysis of Systems, TACAS ’98. Lecture Notes in Computer Science, vol. 1384, pp. 151–166. Springer, New York (1998) Pop, S.: The SSA representation framework: semantics, analyses and GCC implementation. Ph.D. thesis, École des Mines de Paris (2006) Rideau, L., Serpette, B.P., Leroy, X.: Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. J. Autom. Reason. 40(4), 307–326 (2008) Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proc. FLoC Workshop on Run-Time Result Verification (1999) Rival, X.: Symbolic transfer function-based approaches to certified compilation. In: 31st Symposium Principles of Programming Languages, pp. 1–13. ACM, New York (2004) Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: 15th Symposium Principles of Programming Languages, pp. 12–27. ACM, New York (1988) Shao, Z., Trifonov, V., Saha, B., Papaspyrou, N.: A type system for certified binaries. ACM Trans. Program. Lang. Syst. 27(1), 1–45 (2005) Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine. Springer, New York (2001) Strecker, M.: Formal verification of a Java compiler in Isabelle. In: Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 2392, pp. 63–77. Springer, New York (2002) Strecker, M.: Compiler verification for C0 (intermediate report). Technical report, Université Paul Sabatier, Toulouse (2005) Tristan, J.-B., Leroy, X.: Formal verification of translation validators: a case study on instruction scheduling optimizations. In: 35th Symposium Principles of Programming Languages, pp. 17–27. ACM, New York (2008) Tristan, J.-B., Leroy, X.: Verified validation of Lazy Code Motion. In: Programming Language Design and Implementation 2009, pp. 316–326. ACM, New York (2009) Zuck, L.D., Pnueli, A., Fang, Y., Goldberg, B.: VOC: a translation validator for optimizing compilers. In: COCV’02, Compiler Optimization Meets Compiler Verification. Electronic Notes in Theoretical Computer Science, vol. 65, no. 2, pp. 2–18. Elsevier, Amsterdam (2002)