of VCs.The design of the theorem prover,which is em- [10]X.Leroy.Formal certification of a compiler back-end or: bedded in the compiler to prove pointer-related VCs,is also programming a compiler with a proof assistant.In POPL skipped in this paper. '06:Conference record of the 33rdACM SIGPLAN-SIGACT We are improving PointerC and its certifying com- symposium on Principles of programming languages,pages piler:relaxing the restrictions on pointer arithmetic op- 42-54,New York,NY,USA,2006.ACM Press. erations and allowing calloc which is often used in pro- [11]Z.Li.Cog implementation of the soundness proof of fcap grams.We are also studying an embedded theorem prover (description).http://ssg.ustcsz.edu.cn/Iss/software/index. html. for integer-related VCs,and exploring the possibilities to [12]Z.Li.A framework of function-based certified assembly replace the current proof-assistant tool.The influences of programming.http://ssg.ustcsz.edu.cn/lss/doc/index.html. proof-carrying compilation on code optimizations are also [13]Y.Mandelbaum,D.Walker,and R.Harper.An effective the- under consideration. ory of type refinements.In ICFP'03:Proceedings of the eighth ACM SIGPLAN international conference on Func- 8.Acknowledgements tional programming,pages 213-225,New York,NY,USA, 2003.ACM Press. [14]J.S.Moore.Piton:a mechanically verified assembly- We thank Professor Zhong Shao in Yale University and language.Kluwer Academic Publishers,Norwell,MA anonymous referees for suggestions and comments on an 1996. earlier version of this paper.This research is based on work [15]G.Morrisett,D.Walker,K.Crary,and N.Glew.From supported in part by grants from Intel China Research Cen- system f to typed assembly language.In POPL '98:Pro- ter and National Natural Science Foundation of China under ceedings of the 25th ACM SIGPLAN-SIGACT symposium on Grant No.60673126.Any opinions,findings and conclu- Principles of programming languages,pages 85-97,New sions contained in this document are those of the authors York.NY,USA.1998.ACM Press. [16]G.C.Necula.Proof-carrying code.In POPL '97:Pro- and do not reflect the views of these agencies. ceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages,pages 106-119,New References York,NY,USA.1997.ACM Press. [17]G.C.Necula and P.Lee.The design and implementation [1]A.W.Appel.Foundational proof-carrying code.In L/CS of a certifying compiler.In PLDI '98:Proceedings of the '0l:Proceedings of the 16th Annual IEEE Symposium on ACM SIGPLAN 1998 conference on Programming language Logic in Computer Science,pages 247-258.Washington, design and implementation,pages 333-344,New York,NY. DC,USA,2001.IEEE Computer Society. USA.1998.ACM Press. [2]Y.Chen,B.Hua,L.Ge,and W.Zhifang. [18]H.Xi.Applied type system (extended abstract).In post- pointer logic for safety verification of pointer programs. workshop Proceedings of TYPES 2003.pages 394-408. http://ssg.ustcsz.edu.cn/lss/papers/index.html. Springer-Verlag LNCS 3085,2004. [3]C.Colby,P.Lee,G.C.Necula,F.Blau,M.Plesko,and [19]D.Yu,N.A.Hamid,and Z.Shao.Building certified libraries K.Cline.A certifying compiler for java.In PLD/'00: for pcc:dynamic storage allocation.Sci.Comput.Program.. Proceedings of the ACM SIGPLAN 2000 conference on Pro- 50(1-3):101-127.2004. gramming language design and implementation,pages 95- 107.New York.NY.USA.2000.ACM Press. [4]Cog Development Team.The Cog proof assistant reference manual.Cog release v8.0,Oct.2005. [5]E.W.Dijkstra.A discipline of programming.Prentice-Hall, Englewood Cliffs,New Jersey,1976. [6]X.Feng.Z.Shao,A.Vaynberg.S.Xiang.and Z.Ni.Mod- ular verification of assembly code with stack-based con- trol abstractions.In PLDI '06:Proceedings of the 2006 ACM SIGPLAN conference on Programming language de- sign and implementation,pages 401-414,New York,NY, USA.2006.ACM Press. [7]N.A.Hamid,Z.Shao,V.Trifonov,S.Monnier,and Z.Ni. A syntactic approach to foundational proof-carrying code. In LICS'02:Proceedings of the Seventeenth Annual IEEE Symposium on Logic In Computer Science,pages 89-100, Copenhagen,Denmark,July 2002.IEEE. [8]T.Hoare.The verifying compiler:A grand challenge for computing research.J.ACM,50(1):63-69.2003. [9]B.Hua and L.Ge.The definition of pointerc programming language.http://ssg.ustcsz.edu.cn/lss/doc/index.htmlof VCs. The design of the theorem prover, which is em￾bedded in the compiler to prove pointer-related VCs, is also skipped in this paper. We are improving PointerC and its certifying com￾piler: relaxing the restrictions on pointer arithmetic op￾erations and allowing calloc which is often used in pro￾grams. We are also studying an embedded theorem prover for integer-related VCs, and exploring the possibilities to replace the current proof-assistant tool. The influences of proof-carrying compilation on code optimizations are also under consideration. 8. Acknowledgements We thank Professor Zhong Shao in Yale University and anonymous referees for suggestions and comments on an earlier version of this paper. This research is based on work supported in part by grants from Intel China Research Cen￾ter and National Natural Science Foundation of China under Grant No.60673126. Any opinions, findings and conclu￾sions contained in this document are those of the authors and do not reflect the views of these agencies. References [1] A. W. Appel. Foundational proof-carrying code. In LICS ’01: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, pages 247–258, Washington, DC, USA, 2001. IEEE Computer Society. [2] Y. Chen, B. Hua, L. Ge, and W. Zhifang. A pointer logic for safety verification of pointer programs. http://ssg.ustcsz.edu.cn/lss/papers/index.html. [3] C. Colby, P. Lee, G. C. Necula, F. Blau, M. Plesko, and K. Cline. A certifying compiler for java. In PLDI ’00: Proceedings of the ACM SIGPLAN 2000 conference on Pro￾gramming language design and implementation, pages 95– 107, New York, NY, USA, 2000. ACM Press. [4] Coq Development Team. The Coq proof assistant reference manual. Coq release v8.0, Oct. 2005. [5] E. W. Dijkstra. A discipline of programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976. [6] X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Mod￾ular verification of assembly code with stack-based con￾trol abstractions. In PLDI ’06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language de￾sign and implementation, pages 401–414, New York, NY, USA, 2006. ACM Press. [7] N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof-carrying code. In LICS’02: Proceedings of the Seventeenth Annual IEEE Symposium on Logic In Computer Science, pages 89–100, Copenhagen, Denmark, July 2002. IEEE. [8] T. Hoare. The verifying compiler: A grand challenge for computing research. J. ACM, 50(1):63–69, 2003. [9] B. Hua and L. Ge. The definition of pointerc programming language. http://ssg.ustcsz.edu.cn/lss/doc/index.html. [10] X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL ’06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 42–54, New York, NY, USA, 2006. ACM Press. [11] Z. Li. Coq implementation of the soundness proof of fcap (description). http://ssg.ustcsz.edu.cn/lss/software/index. html. [12] Z. Li. A framework of function-based certified assembly programming. http://ssg.ustcsz.edu.cn/lss/doc/index.html. [13] Y. Mandelbaum, D. Walker, and R. Harper. An effective the￾ory of type refinements. In ICFP’03: Proceedings of the eighth ACM SIGPLAN international conference on Func￾tional programming, pages 213–225, New York, NY, USA, 2003. ACM Press. [14] J. S. Moore. Piton: a mechanically verified assembly￾language. Kluwer Academic Publishers, Norwell, MA, 1996. [15] G. Morrisett, D. Walker, K. Crary, and N. Glew. From system f to typed assembly language. In POPL ’98: Pro￾ceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 85–97, New York, NY, USA, 1998. ACM Press. [16] G. C. Necula. Proof-carrying code. In POPL ’97: Pro￾ceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 106–119, New York, NY, USA, 1997. ACM Press. [17] G. C. Necula and P. Lee. The design and implementation of a certifying compiler. In PLDI ’98: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, pages 333–344, New York, NY, USA, 1998. ACM Press. [18] H. Xi. Applied type system (extended abstract). In post￾workshop Proceedings of TYPES 2003, pages 394–408. Springer-Verlag LNCS 3085, 2004. [19] D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for pcc: dynamic storage allocation. Sci. Comput. Program., 50(1-3):101–127, 2004