面向源代码的软件模型检测及其实现

模型检测应用于检测软件可靠性具有重要意义。介绍了一种基于谓词抽象和反例引导抽象求精技术对源程序进行建模和验证的模型检测方法，并结合自行研发的jchecker工具详细介绍了该软件模型检测技术的运作过程和关键算法。