论文部分内容阅读
提出了一种用模型检验技术对程序进行分析的方法，其主要思想是将C/C＋＋源代码转换为与控制流图等价的Kripke结构，用CTL公式描述待验证的源程序性质，使用NuSMV模型检验工具实施具体的程序分析。基于这一思想，设计并实现了一个自动将C/C＋ }源代码转换为NuSMV输入的工具。所做的实验验证表明，该方法能够有效地对程序进行分析。