论文部分内容阅读
形式验证是提高软件可信程度的重要方法，基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点，但尚无可供工业界使用的产品，其根源在于自动定理证明方面的困难．介绍在通过程序分析建立起各程序点的形状图的基础上，如何利用形状图提供的信息来支持程序验证的方法．提出一种利用形状图信息来消除访问路径别名，使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法，并证明了该方法的可靠性．还提出一种在不使用自定义谓词的情况下，易变数据结构上数据性质的描述和验证方法．另外，介绍所设计并实现的基于上述方法的P