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

龙图腾网恭喜浙江大学申请的专利一种用于Java软件的形式化验证方法及装置获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN115357492B 。

龙图腾网通过国家知识产权局官网在2025-05-30发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202210998284.2，技术领域涉及：G06F11/3604；该发明授权一种用于Java软件的形式化验证方法及装置是由赵永望;陆嘉晨;沈韬立;常瑞;任奎设计研发完成，并于2022-08-19向国家知识产权局提交的专利申请。

本一种用于Java软件的形式化验证方法及装置在说明书摘要公布了：本发明公开了一种用于Java软件的形式化验证方法及装置。本发明将Java代码转换为一种中间表示语言，并对该中间表示语言进行建模，再由相关形式化验证人员根据不同模型的功能需求文档描述程序规约并证明。由于中间语言的语义较为简单，有较少的未定义行为，因此本发明基于中间语言的形式化验证，通过将Java代码转换为中间表示代码，避免了形式化验证系统需要对复杂的Java语言模型进行建模和验证，降低了对于Java语言的形式化验证的难度，也减少了对于形式化验证人员的个人素质依赖。通过基于SMT求解器的形式化验证方式，提高了形式化验证的自动化程度，降低了形式化验证的数学难度和形式化验证的门槛。

本发明授权一种用于Java软件的形式化验证方法及装置在权利要求书中公布了：1.一种用于Java软件的形式化验证方法，其特征在于，包括S1:获得Java程序源代码，并对Java程序源代码进行词法分析、语法分析和语义分析，生成Java扩展抽象语法树；S2:解析出Java扩展抽象语法树中的常量、变量、继承关系和函数限定符，为其分配内存地址，生成中间表示代码；S3:对Java程序需求文档进行自动化建模，翻译成对应的Java形式化规约，其中，形式化规约主要包括Java程序的表达不变式、安全性；S4:解析Java程序规约，将形式化人员定义的Java程序规约转换成对应的Java程序规约的SMT表达式；S5:解析步骤S3中的中间表示代码的指令含义，根据指令含义将代码转换为符号值，根据符号值转换为对应Java程序实现的SMT表达式；S6:对S4中产生的Java程序规约的SMT表达式和S5中产生的Java程序实现的SMT表达式的精化关系进行求解，若存在精化关系，则说明通过形式化验证，否则生成对应用的反例用说明，得到验证结果；S7:接受验证结果，生成形式化验证结果报告。

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