2 A pointer logic and certifying compiler specified or reasoned about.The other is the research on certifying compilation. which explores how the compiler generates proofs for the compiled programs For the first challenge,the TAL (Typed Assembly Language)project [2] and the theory of type refinements 3 are two typical projects in type-based approaches,while PCC [1]and FPCC(Foundational Proof-Carrying Code)[4] are typical projects on logic-based techniques.Type-based and logic-based tech- niques are complementary to each other,and in recent years,some researchers have tried to combine those techniques.Shao et al.adopted a syntactic approach to FPCC,and proposed a simple and flexible framework to support Hoare-style reasoning for assembly code certification in their projects CAP(Certified Assem- bly Programming)[5]and SCAP (Stack-based CAP)[6]etc.The ATS (Applied Type System)project 7 proposed by Xi et al.extends the type system with a notion of program states,so that invariants on states could be captured in state- ful programming.By encoding Hoare logic in its type system,ATS can support Hoare-logic-like reasoning via the type system. For the second challenge,Necula implemented a certifying compiler [8]called Touchstone.It contains a traditional compiler for a small but type-safe subset of C and a certifier that automatically produces a proof of type safety for each assembly program produced by the compiler.Later,Colby et al.implemented Special J 9,a certifying compiler for a large subset of Java.It compiles Java byte code into target code for Intel's IA32 architecture. We have adopted PCC technology and certifying compilation to a program- ming language with dynamic storage allocation and deallocation-PointerCl(a safe C-like language defined in our work).And we have also implemented a certifying compiler prototype for PointerC.Pointer operations in PointerC are restricted:pointer variables can only be used in assignment,equality compari- son,dereference or as the parameters of functions:the address-of operator (& and pointer arithmetic are forbidden.We adopt an approach combining both type-based and logic-based techniques to reason about program properties.To make the type system simple and guarantee the safety of the language at the same time,side conditions are introduced into the typing rules to express the constraints on values.In order to check these side conditions statically,we have designed a pointer logic for PointerC.The pointer logic is an extension of Hoare logic and essentially is a pointer analysis tool.It collects pointer information in a forward manner.Such information can be used to prove that the program sat- isfies the side conditions in the typing rules and then to support value-sensitive static checking. The pointer logic is the main contribution of this paper.As extensions of Hoare logic,separation logic 10 and our pointer logic are both to reason about properties of pointer programs for shared mutable data structures.But there is a great difference between them.Our pointer logic concerns pointer aliasing.In the pointer logic,different access paths are assumed to be bound to different storage locations,unless it can be proved that they are bound to the same location 1 Hua B J and Ge L.The definition of PointerC programming language. http://ssg.ustcsz.edu.cn/Iss/doc/index.html.(in Chinese)2 A pointer logic and certifying compiler specified or reasoned about. The other is the research on certifying compilation, which explores how the compiler generates proofs for the compiled programs. For the first challenge, the TAL (Typed Assembly Language) project [2] and the theory of type refinements [3] are two typical projects in type-based approaches, while PCC [1] and FPCC (Foundational Proof-Carrying Code) [4] are typical projects on logic-based techniques. Type-based and logic-based tech￾niques are complementary to each other, and in recent years, some researchers have tried to combine those techniques. Shao et al. adopted a syntactic approach to FPCC, and proposed a simple and flexible framework to support Hoare-style reasoning for assembly code certification in their projects CAP (Certified Assem￾bly Programming) [5] and SCAP (Stack-based CAP) [6] etc. The ATS (Applied Type System) project [7] proposed by Xi et al. extends the type system with a notion of program states, so that invariants on states could be captured in state￾ful programming. By encoding Hoare logic in its type system, ATS can support Hoare-logic-like reasoning via the type system. For the second challenge, Necula implemented a certifying compiler [8] called Touchstone. It contains a traditional compiler for a small but type-safe subset of C and a certifier that automatically produces a proof of type safety for each assembly program produced by the compiler. Later, Colby et al. implemented Special J [9], a certifying compiler for a large subset of Java. It compiles Java byte code into target code for Intel’s IA32 architecture. We have adopted PCC technology and certifying compilation to a program￾ming language with dynamic storage allocation and deallocation—PointerC1 (a safe C-like language defined in our work). And we have also implemented a certifying compiler prototype for PointerC. Pointer operations in PointerC are restricted: pointer variables can only be used in assignment, equality compari￾son, dereference or as the parameters of functions; the address-of operator (&) and pointer arithmetic are forbidden. We adopt an approach combining both type-based and logic-based techniques to reason about program properties. To make the type system simple and guarantee the safety of the language at the same time, side conditions are introduced into the typing rules to express the constraints on values. In order to check these side conditions statically, we have designed a pointer logic for PointerC. The pointer logic is an extension of Hoare logic and essentially is a pointer analysis tool. It collects pointer information in a forward manner. Such information can be used to prove that the program sat￾isfies the side conditions in the typing rules and then to support value-sensitive static checking. The pointer logic is the main contribution of this paper. As extensions of Hoare logic, separation logic [10] and our pointer logic are both to reason about properties of pointer programs for shared mutable data structures. But there is a great difference between them. Our pointer logic concerns pointer aliasing. In the pointer logic, different access paths are assumed to be bound to different storage locations, unless it can be proved that they are bound to the same location 1 Hua B J and Ge L. The definition of PointerC programming language. http://ssg.ustcsz.edu.cn/lss/doc/index.html. (in Chinese)