摘要：为了解决谓词抽象技术面临的程序中循环体的每次迭代都至少需要一个谓词来实现的难题,提出了一个两阶段的不完全判定过程,用来对一个包含循环的反例进行可行性模拟。通过给出的循环探测算法来从抽象模型中提取出包含循环的反例,并用循环迭代的数量作为参数来确定模拟实例。实验结果表明,该方法在典型的缓冲溢出实例中的表现优于传统的抽象求精方法。

摘要：随着软硬件设计的规模越来越大,功能越来越复杂,往往导致形式化验证出现"组合爆炸"问题,而谓词抽象方法是解决状态空间"组合爆炸"问题的重要技术之一。面向硬件的谓词抽象方法是不可满足子式的典型应用,通过求解不可满足子式,能够减少谓词抽象过程中精化迭代的次数,从而提高形式化验证效率。针对微处理器的指令Cache部件,将两种最小不可满足子式的求解算法进行了比较,结果表明贪心遗传算法在运行效率方面优于分支-限界算法。并且深入分析了不可满足子式在硬件谓词抽象中的作用,以及如何加速芯片的形式化验证过程。

摘要：谓词抽象是解决软件模型检查中状态空间爆炸的最有效方法之一,针对Java语言面向对象的特性,描述了一种对Java程序语言中间形式的谓词抽象算法,该算法将Java程序抽象成为布尔程序,抽象过程中处理的Java数据结构包括:赋值语句、条件语句、类对象引用、成员方法和方法调用等。用一个Java程序实例说明了该算法的抽象过程和结果。

摘要：高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导。