一种基于错误状态树的IC3算法优化方法及系统

本发明公开了一种基于错误状态树的IC3算法优化方法及系统，本发明方法包括获取被验证程序的带有属性的Lustre模型文件，利用模型检查工具中优化后的IC3算法迭代求解以获得验证结果以及错误状态树，且利用优化后的IC3算法迭代求解时包括在IC3算法的每一个Block过程利用建好的错误状态树实现错误状态的复用以缩减错误状态路径并减少IC3算法执行过程中的约束求解次数。本发明旨在利用优化后的IC3算法迭代求解时包括在IC3算法的每一个Block过程利用建好的错误状态树实现错误状态的复用以缩减错误状态路径并减少IC3算法执行过程中的约束求解次数，提高IC3算法中错误状态的求解效率。