%0 Journal Article
%T Pointer Logic Dealing with Uncertain Equality of Pointers<br>处理指针相等关系不确定的指针逻辑
%A LIANG Hong-Jin
%A ZHANG Yu
%A CHEN Yi-Yun
%A LI Zhao-Peng
%A HUA Bao-Jian
%A <br>梁红瑾
%A 张昱
%A 陈意云
%A 李兆鹏
%A 华保健
%J 软件学报
%D 2010
%I 
%X A pointer logic is designed for a C-like programming language PointerC. The pointer logic is an extension of Hoare logic, and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated. This paper presents an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets, so as to reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers is uncertain.
%K software safety
%K Hoare logic
%K pointer logic<br>软件安全
%K Hoare逻辑
%K 指针逻辑
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=DA18E85CD4575B568726E7E342DF0DBD&yid=140ECF96957D60B2&vid=659D3B06EBF534A7&iid=0B39A22176CE99FB&sid=9DC563A0FEFC04F9&eid=5957D6E0A50D26B5&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=17