C程序控制流程模型的提取技术与实现

摘要：

控制流图描述了函数执行时可能采取的执行路径.绝大多数静态分析工具都在抽象语法树之上生成控制流图并据此对程序的运行行为进行分析.在模型检测过程中,提取正确的控制流图是构建系统模型的关键.在分析C程序的抽象语法树和控制结构的基础上,设计并实现了程序控制流图提取的算法,并分析了算法的正确性.基于提取的控制流程,可对C程序的某些性质进行模型检验.

关键词：控制流图、抽象语法树、模型检测

所属期刊栏目：41

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金项目61073050,61170044

在线出版日期：2014-06-03（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：208-214