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

龙图腾网获悉浙江大学申请的专利一种用于ESBMC的形式化规约生成与验证方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN121070759B 。

龙图腾网通过国家知识产权局官网在2026-02-17发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202511620491.4，技术领域涉及：G06F11/3604；该发明授权一种用于ESBMC的形式化规约生成与验证方法是由赵永望;许智围设计研发完成，并于2025-11-07向国家知识产权局提交的专利申请。

本一种用于ESBMC的形式化规约生成与验证方法在说明书摘要公布了：本发明公开了一种用于ESBMC的形式化规约生成与验证方法，通过结合大语言模型与ESBMC工具，减少了人工干预，能够显著提升复杂程序的验证效率和准确性，在处理包含复杂控制结构的程序时，自动生成的规约能够充分反映程序的真实行为；通过利用大语言模型分析提取的程序信息，自动生成前置条件、后置条件以及循环不变量形式化规约，将其输入到ESBMC工具中进行验证，得到验证结果。通过将ESBMC的验证结果反馈到规约生成模块，对生成的规约进行细化和修复，并通过动态调整生成策略，针对不同的程序行为进行优化，确保生成的形式化规约准确有效。通过监督微调和强化训练持续优化大语言模型的能力，使得模型能够自动适应不同程序的特性，生成更精确的规约。

本发明授权一种用于ESBMC的形式化规约生成与验证方法在权利要求书中公布了：1.一种用于ESBMC验证的形式化规约生成与验证方法，其特征在于，包括： S1：获得CC++程序源代码，并提取程序中的变量、函数、控制流以及其他关键程序结构； S2：使用大语言模型分析提取的信息，初步生成符合ESBMC验证要求的形式化规约，其中，所生成的规约主要包括前置条件、后置条件以及循环不变量； S3：将S2中生成的形式化规约输入到ESBMC工具中进行验证，得到ESBMC的验证结果； S4：使用S3中ESBMC的验证结果细化和修复生成的规约，得到通过ESBMC验证的规约数据；若验证结果表明规约存在问题，将根据验证失败的原因调整生成策略细化和修复生成的规约，得到验证失败以及修复过程的规约数据； S5：通过S4过程中搜集的通过ESBMC验证的规约数据，用这批数据对大模型进行监督微调； S6：通过S4过程中搜集的验证成功和失败以及修复过程的规约数据，用这批数据对大模型进行进一步的强化训练； S7：输出最终验证规约，生成验证结果。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人浙江大学，其通讯地址为：310058 浙江省杭州市西湖区余杭塘路866号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。

以上内容由龙图腾AI智能生成。