指针类型递归函数前后形状图的自动推断  

Automatic Inference of Pre and Post Shape Graphs for Pointer-type Recursive Functions

作　　者：宋艳辉[1,2] 李兆鹏[1,2] 陈意云[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026 [2]中国科学科技大学苏州研究院软件安全实验室,江苏苏州215123

出　　处：《小型微型计算机系统》2014年第4期759-764,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61170018;61003043;61229201)资助

摘　　要：在一个基于形状图逻辑的自动程序验证原型系统上,设计与实现了指针类型递归函数前后形状图的自动推断方法.该方法类似于循环不变形状图的推断方法,区别在于它首先沿着函数的非递归路径,从函数入口的函数前形状图推断函数出口的函数后形状图的初值,然后沿着函数的递归路径对函数后形状图进行迭代求解.本文还设计了上述自动推断方法中需要用到的形状图之间蕴涵关系的判定方法.本文方法使得原型系统扩展到能够自动验证指针类型的递归函数.By extending an existing automatic program verification prototype system based on shape graph logic, this paper puts for- ward a method for inferring pre and post shape graphs for pointer-type recursive functions. While this method is similar to the infer- ence method for loop-invariant shape graphs, it infers initial post shape graph at function＇s exit from its entrance＇s pre shape graph through non-recursive paths and then infers its post shape graph iteratively through recursive paths. Besides, the paper designs the de- cision method for implication between shape graphs used by the inferring method above. The paper makes it possible for the prototype system to automatically verify pointer-type recursive functions.

关 键 词：程序验证 形状图逻辑 形状分析 递归函数 不变式的自动推断 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]