← 返回列表
一种针对复杂数据处理需求的高效形式化代码构建方法
摘要文本
本发明公开了一种针对复杂数据处理需求的高效形式化代码构建方法，包括：通过F*语言提取所要构建的代码的数学逻辑；将所述数学逻辑基于HACL*库和Low*库进行构建实现，其中通过对HACL*库进行扩展以应对复杂数据处理需求；编译执行所述代码，以完成从规范到实现的正确性验证和内存安全性验证；通过kremlin工具自动将已验证的Low*转换为语义等效的C代码。
申请人信息
- 申请人:浙江大学; 浙江大学嘉兴研究院
- 申请人地址:310058 浙江省杭州市西湖区余杭塘路866号
- 发明人: 浙江大学; 浙江大学嘉兴研究院
专利详细信息
| 项目 | 内容 |
|---|---|
| 专利名称 | 一种针对复杂数据处理需求的高效形式化代码构建方法 |
| 专利类型 | 发明申请 |
| 申请号 | CN202311506458.X |
| 申请日 | 2023/11/13 |
| 公告号 | CN117591087A |
| 公开日 | 2024/2/23 |
| IPC主分类号 | G06F8/30 |
| 权利人 | 浙江大学; 浙江大学嘉兴研究院 |
| 发明人 | 张秉晟; 张跃耀; 任奎 |
| 地址 | 浙江省杭州市西湖区余杭塘路866号; 浙江省嘉兴市智富中心48幢401室 |
专利主权项内容
1.一种针对复杂数据处理需求的高效形式化代码构建方法，其特征在于，包括：建立规范：通过F*语言提取所要构建的代码的数学逻辑；构建实现：将所述数学逻辑基于HACL*库和Low*库进行构建实现，其中通过对HACL*库进行扩展以应对复杂数据处理需求；验证代码：编译执行所述代码，以完成从规范到实现的正确性验证和内存安全性验证；代码生成：通过kremlin工具自动将已验证的Low*转换为语义等效的C代码。