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

龙图腾网获悉安徽大学申请的专利一种降低数据结构形式化验证难度的程序处理方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN116501633B 。

龙图腾网通过国家知识产权局官网在2026-02-13发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202310457358.6，技术领域涉及：G06F11/3604；该发明授权一种降低数据结构形式化验证难度的程序处理方法是由李薛剑;余韵设计研发完成，并于2023-04-25向国家知识产权局提交的专利申请。

本一种降低数据结构形式化验证难度的程序处理方法在说明书摘要公布了：本发明提供一种降低数据结构形式化验证难度的程序处理方法，在处理复杂数据结构中带有全称量化断言的验证条件时，首先通过嵌套形状图，对复杂数据结构进行刻画；并结合分析主数据结构和次数据结构的形状定义，得到最终嵌套形状图的形状定义；然后通过对断言中包含全称量化断言的谓词和宏定义进行展开，基于演绎推理遍历和匹配所有断言，根据匹配的结果进行相应的拆分和拼接处理，得到新的断言。本发明针对全称量化断言的复杂数据结构程序，采用拆分和拼接方式，大大降低了形式化验证的复杂度，从而有效降低了数据结构程序验证难度，提高了验证效率。

本发明授权一种降低数据结构形式化验证难度的程序处理方法在权利要求书中公布了：1.一种降低数据结构形式化验证难度的程序处理方法，其特征在于，具体包括以下步骤： S1、通过嵌套形状图对复杂数据结构程序进行刻画：针对带有全称量化断言的复杂数据结构程序，利用嵌套形状图将其拆分为多个便于分别进行验证的基本形状图； S2、对基本形状图对应的全称量化断言进行拆分和拼接，得到新的断言：对包含全称量化断言的蕴含式进行全称量化断言的谓词和宏定义展开，基于演绎推理遍历和匹配所有断言，根据匹配的结果进行拆分和拼接处理；具体包括： S21、分别获取所述蕴含式的前件和后件的所有全称量化断言，并将前件和后件中的所有全称量化断言分别定义为集合E1和E2； S22、依次遍历所述集合E1和E2中的每一个全称量化断言，并在前件的全称量化断言集合E1中查找与后件的全称量化断言集合E2匹配的所有断言，得到匹配断言集合Match； S23、当所述匹配断言集合match中元素的个数大于1时，对前件断言集合E1中的全称量化断言进行拼接； S24、当所述匹配断言集合match中元素的个数等于1时，对后件断言集合E2中的全称量化断言进行拆分。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人安徽大学，其通讯地址为：230601 安徽省合肥市经济技术开发区九龙路111号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。

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