买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网恭喜中国人民解放军国防科技大学申请的专利一种基于不可满足核的IC3加速验证方法及系统获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN118897808B 。

龙图腾网通过国家知识产权局官网在2025-03-11发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202411388748.3，技术领域涉及：G06F11/3604；该发明授权一种基于不可满足核的IC3加速验证方法及系统是由尹良泽;龚欣怡;董威;王戟;李姗姗;陈振邦;刘万伟设计研发完成，并于2024-10-08向国家知识产权局提交的专利申请。

本一种基于不可满足核的IC3加速验证方法及系统在说明书摘要公布了：本发明公开了一种基于不可满足核的IC3加速验证方法及系统，本发明包括将待验证的程序模型输入采用SMT求解器的IC3算法模型进行求解以获得待验证的程序模型是否满足指定的安全属性或规范的验证结果，且包括初始化不可满足核库，每一次调用SMT求解器前检查不可满足核库，如果找到与当前公式匹配的不可满足核则跳过求解过程，否则才执行求解并在求解后将返回的不可满足核更新到不可满足核库中。本发明旨在利用IC3算法中大量约束求解间具有相似性，根据前面约束求解构建不可满足核库，基于已有的不可满足核心快速实现后面部分问题的求解可以减少SMT求解次数从而减少IC3算法的运行时间，加速IC3算法的验证速度。

本发明授权一种基于不可满足核的IC3加速验证方法及系统在权利要求书中公布了：1.一种基于不可满足核的IC3加速验证方法，用于对使用Lustre语言进行建模的软件程序模型进行验证，其特征在于，所述IC3加速验证方法包括将待验证的程序模型的Lustre文件输入采用SMT求解器的IC3算法模型进行求解以获得待验证的程序模型是否满足指定的安全属性或规范的验证结果，且采用SMT求解器的IC3算法模型进行求解包括：初始化不可满足核库，所述不可满足核库用于存储之前求解过程中从求解器获得的不可满足核，在IC3算法模型每一次调用SMT求解器进行公式求解前检查不可满足核库，如果在不可满足核库中找到与当前公式匹配的不可满足核则直接获取该不可满足核并跳过本次调用SMT求解器的求解过程，否则才调用SMT求解器进行公式求解；在调用SMT求解器进行公式求解后，如果SMT求解器判定当前公式不可满足则将SMT求解器返回的不可满足核更新到不可满足核库中；如果SMT求解器判定当前公式可满足则SMT求解器返回的满足当前公式的一组赋值；所述不可满足核库包括用于存储下式所示公式匹配的不可满足核的不可满足核库： ，上式中，为安全属性，用于软件系统应该满足的安全条件或约束；为forward状态集合，forward状态集合是从初始状态集合I出发通过k步迁移关系T后可达的状态集合，forward状态集合为合取范式，其格式为，其中～为子句，为逻辑与；为一步转移关系；为子句，子句，其中～为文字，为逻辑或；为子句经过一步迁移后的否定状态，为逻辑非；所述不可满足核库还包括用于存储下式所示公式匹配的不可满足核的不可满足核库： ，上式中，为初始状态集合，为子句，子句，其中～为文字，为逻辑或，为逻辑与，为逻辑非；所述IC3算法模型的执行步骤包括：初始化循环变量k；forward过程：执行IC3算法的forward求解并调用SMT求解器进行公式求解，如果求解后达到不动点，则判定属性成立，待验证的程序模型满足指定的安全属性或规范的验证结果，结束并退出；如果求解后未达到不动点，则进入block过程；block过程：执行IC3算法的block过程求解并调用SMT求解器进行公式求解，如果求解后发现真实反例，则判定属性不成立，待验证的程序模型不满足指定的安全属性或规范的验证结果，结束并退出；如果未发现真实反例，则将循环变量k加1并进入forward过程。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人中国人民解放军国防科技大学，其通讯地址为：410073 湖南省长沙市开福区德雅路109号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。