梁红瑾等：处理指针相等关系不确定的指针逻辑 343 [8]Chen YY,Ge L,Hua BJ,Li ZP,Liu C.Design of a certifying compiler supporting proof of program safety.In:Proc.of the Ist IEEE/IFIP Int'l Symp.on Theoretical Aspects of Software Engineering.Shanghai:IEEE Computer Society Press,2007.127-136. [9]Schorr H,Waite WM.An efficient machine independent procedure for garbage collection in various list structures. Communications of the ACM,1967,10(8):501-506. [10]Hubert T,Marche C.A case study of C source code verification:The Schorr-Waite algorithm.In:Aicherig BK,Beckert B,eds. Proc.of the 3rd IEEE Int'l Conf.on Software Engineering and Formal Methods.Koblenz:IEEE Computer Society Press,2005. 190-199. [11]The Glibe contributors.http://www.gnu.org/software/libe/ [12]Liang HJ,Zhang Y,Chen YY,Li ZP,Hua BJ.An example of reasoning in extended pointer logic:AlO remove request function in Glibc.Technical Report.http://home.ustc.edu.cn/-Ihj1018/ [13]Bornat R.Proving pointer programs in Hoare logic.In:Backhouse RC,Oliveira JN,eds.Proc.of the 5th Int'l Conf.on Mathematics of Program Construction.LNCS 1837,Ponte de Lima:Springer-Verlag,2000.102-126. [14]Bornat R,Calcagno C,O'Hearn PW.Local reasoning,separation and aliasing.In:Proc.of the 2nd Workshop on Semantics, Program Analysis,and Computing Environments for Memory Management.2004. [15]Yang H.An example of local reasoning in BI pointer logic:The Schorr-Waite graph marking algorithm.In:Henglein F,Hughes J, Makholm H,Niss H,eds.Proc.of the Ist Workshop on Semantics,Program Analysis and Computing Environments for Memory Management.London:IT University of Copenhagen,2001.41-68. 附中文参考文献： [3)陈意云，华保健，葛琳，王志芳.一种用于指针程序安全性证明的指针逻辑.计算机学报，2008,31(3372-380. [)门华保健，陈意云，李兆鹏，王志芳，葛琳.安全语言PointerC的设计及形式证明.计算机学报，2008,31(4)：556-564. 梁红瑾(1989一)，女，江苏徐州人，硕士生 李兆鹏(1978-)，男，博士，CCF会员，主要 主要研究领域为程序验证，软件安全. 研究领域为程序验证，软件安全，类型系统 和理论 张昱(1972-)，女，博士，副教授，CCF会员， 华保健(1979-)，男，博士，CC下学生会员， 主要研究领域为程序设计语言理论与 主要研究领域为程序设计语言的设计与 实现 实现软件安全 陈意云(1946-)，男，教授，博士生导师，CC℉ 高级会员，主要研究领域为程序设计语言 理论和实现技术，程序验证，软件安全 @中国科学院软件研究所htp:www.c-s-a.org.cn梁红瑾 等:处理指针相等关系不确定的指针逻辑 343 [8] Chen YY, Ge L, Hua BJ, Li ZP, Liu C. Design of a certifying compiler supporting proof of program safety. In: Proc. of the 1st IEEE/IFIP Int’l Symp. on Theoretical Aspects of Software Engineering. Shanghai: IEEE Computer Society Press, 2007. 127−136. [9] Schorr H, Waite WM. An efficient machine independent procedure for garbage collection in various list structures. Communications of the ACM, 1967,10(8):501−506. [10] Hubert T, Marché C. A case study of C source code verification: The Schorr-Waite algorithm. In: Aichernig BK, Beckert B, eds. Proc. of the 3rd IEEE Int’l Conf. on Software Engineering and Formal Methods. Koblenz: IEEE Computer Society Press, 2005. 190−199. [11] The Glibc contributors. http://www.gnu.org/software/libc/ [12] Liang HJ, Zhang Y, Chen YY, Li ZP, Hua BJ. An example of reasoning in extended pointer logic: AIO remove request function in Glibc. Technical Report. http://home.ustc.edu.cn/~lhj1018/ [13] Bornat R. Proving pointer programs in Hoare logic. In: Backhouse RC, Oliveira JN, eds. Proc. of the 5th Int’l Conf. on Mathematics of Program Construction. LNCS 1837, Ponte de Lima: Springer-Verlag, 2000. 102−126. [14] Bornat R, Calcagno C, O’Hearn PW. Local reasoning, separation and aliasing. In: Proc. of the 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management. 2004. [15] Yang H. An example of local reasoning in BI pointer logic: The Schorr-Waite graph marking algorithm. In: Henglein F, Hughes J, Makholm H, Niss H, eds. Proc. of the 1st Workshop on Semantics, Program Analysis and Computing Environments for Memory Management. London: IT University of Copenhagen, 2001. 41−68. 附中文参考文献: [3] 陈意云,华保健,葛琳,王志芳.一种用于指针程序安全性证明的指针逻辑.计算机学报,2008,31(3):372−380. [7] 华保健,陈意云,李兆鹏,王志芳,葛琳.安全语言 PointerC 的设计及形式证明.计算机学报,2008,31(4):556−564. 梁红瑾(1989－),女,江苏徐州人,硕士生, 主要研究领域为程序验证,软件安全. 李兆鹏(1978－),男,博士,CCF 会员,主要 研究领域为程序验证,软件安全,类型系统 和理论. 张昱(1972－),女,博士,副教授,CCF 会员, 主要研究领域为程序设计语言理论与 实现. 华保健(1979－),男,博士,CCF 学生会员, 主要研究领域为程序设计语言的设计与 实现,软件安全. 陈意云(1946－),男,教授,博士生导师,CCF 高级会员,主要研究领域为程序设计语言 理论和实现技术,程序验证,软件安全