基于依赖公式抽象的软件模型检测研究

软件形式化验证是国际计算机科学基础研究的前沿领域之一，基于抽象模型检测方法是当前软件形式化验证的研究热点。本项目将抽象解释、模型检测和定理证明等技术有机结合起来，使之能自动验证软件安全性，并在不满足某性质时给出反例。研究利用所验证的公式获得最小谓词集；构造依赖所验证公式的最小近似抽象；在近似抽象模型中确定不合理反例，并使用OBDD布尔满足性问题求解最小谓词集，消除此不合理反例，精化抽象模型；基于抽象解释的完备理论，构造依赖所验证公式的最小完备抽象；根据抽象反例，通过路径仿真技术，确定具体反例路径。.本项目提出依赖所验证公式的弱性质保留抽象，以及依赖所验证公式最小完备抽象的方法，具有学术上的创新性。并力争通过这些研究，使依赖公式的抽象能为软件程序抽象提供一种新的、有效的途径，为软件模型检测提供高效的支持。