Towards formal verification of big data processing

迈向大数据处理的形式化验证

• 批准号: 15K12013
• 负责人: AFFELDT Reynald
• 金额: $ 1.33万
• 依托单位: National Institute of Advanced Industrial Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Challenging Exploratory Research
• 财政年份: 2015
• 资助国家: 日本
• 起止时间: 2015-04-01 至 2018-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-15K12013/
• 关键词: 定理証明支援系; 簡潔データ構造; プログラミング言語OCaml; プログラミング言語C; コード生成器

项目成果

Coqによる簡潔データ構造のライブラリに向けての今後の課題

使用 Coq 构建简洁数据结构库的未来挑战

• 发表时间: 2017
• 作者: 田中 哲;Reynald Affeldt;Jacques Garrigue
• 通讯作者: Jacques Garrigue

Ruby Extension Library Verified using Coq Proof-assistant

使用 Coq Proof-assistant 验证的 Ruby 扩展库

• 发表时间: 2017
• 作者: 田中 哲;Reynald Affeldt;Jacques Garrigue;田中哲
• 通讯作者: 田中哲

Formal Verification for Succinct Data Structures

简洁数据结构的形式化验证

形式的な情報・符号理論のライブラリに向けて

迈向正式的信息/编码理论库

• 发表时间: 2017
• 作者: Reynald Affeldt;Jacques Garrigue;Takafumi Saikawa
• 通讯作者: Takafumi Saikawa

Coq からの C プログラム生成

从 Coq 生成 C 程序

• 发表时间: 2017
• 作者: 田中 哲;Reynald Affeldt;Jacques Garrigue;田中哲;田中哲
• 通讯作者: 田中哲