首页|A Shape Graph Logic and A Shape System

A Shape Graph Logic and A Shape System

扫码查看
原文链接
  • NETL
  • NSTL
  • 万方数据
  • 维普
Analysis and verification of pointer programs are still difficult problems so far.This paper uses a shape graph logic and a shape system to solve these problems in two stages.First,shape graphs at every program point are constructed using an analysis tool.Then,they are used to support the verification of other properties (e.g.,orderedness).Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees,treaps,AVL trees and AA trees,etc.The proposed shape graph logic,as an extension to Hoare logic,uses shape graphs directly as assertions.It can be used in the analysis and verification of programs manipulating mutable data structures.The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage.The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations.It can help rule out programs that construct shapes deviating from what programmers expect (reflected in shape declarations) in the analysis stage.As a benefit,programmers need not provide specifications (e.g.,pre-/post-conditions,loop invariants) about pointers.Moreover,we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs.Thus,verification conditions could be discharged by general theorem provers.

shape graph logicprogram verificationshape analysisautomated theorem provingloop invariant inference

Zhao-Peng Li、Yu Zhang、Yi-Yun Chen

展开 >

School of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China Suzhou 215123, China

This research was supported by the National Natural Science Foundation of China underThis research was supported by the National Natural Science Foundation of China underNational High Technology Research and Development 863 Program of China underand the Postdoctoral Science Foundation of China under

61003043611700182012AA010901-22012M521250

2013

10.1007/s11390-013-1398-1

计算机科学技术学报(英文版)
中国计算机学会

计算机科学技术学报(英文版)

CSTPCDCSCDSCIEI
影响因子：0.432
ISSN：1000-9000
年,卷(期)：2013.28(6)
  • 8
  • 32