Pointer Logic for Verification of Pointer Programs
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    This paper improves and extends the pointer logic that has been designed for verifying pointer programs. Its main contribution is that a concept of legal sets of access paths is presented, which simplifies elementary operations on access paths and makes inference rules of the logic easier to understand. Furthermore, the logic with inference rules is extended for local reasoning and for function construction, making the logic used conveniently in the context of function calls.

    Reference
    Related
    Cited by
Get Citation

陈意云,李兆鹏,王志芳,华保健.一种用于指针程序验证的指针逻辑.软件学报,2010,21(3):415-426

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:January 16,2008
  • Revised:March 31,2009
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063