论文部分内容阅读
程序验证中的常见情景是判断某个用户指定的性质在程序执行之后或执行过程中的某个程序点上是否成立。人工的形式化验证过程繁琐且容易出错,因此形式化验证的自动化是提高代码验证效率的重要方法。数据流分析技术是一种能够自动发现程序中某类性质的技术。研究了将一种数据流分析技术（单链表形状分析）和基于Scope Logic的代码验证过程相结合的方法。通过数据流分析获得所有程序点上的单链表可达性性质,将结果表达为带有递归函数的一阶逻辑公式,并将其插入到相应程序点中。分析程序还根据Scope Logic的证明法则设定了这些公