Development of formally verifiable framework for program transformation

开发可正式验证的程序转型框架

• 批准号: 20500011
• 负责人: NISHIMURA Susumu
• 金额: $ 2.83万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20500011/
• 关键词: プログラム理論; プログラム変換; 形式的証明; 形式的検証; 並行プログラム

We have developed a method, which is an extension of the stepwise refinement method, for correctness-preserving transformation of programs that make use of advanced features such as pointer manipulations and exceptions. We have shown that each feature has a corresponding logical system, namely, separation logic for pointer manipulations and four-valued logic for exceptions. It has been shown that the correctness of programs is formally guaranteed by developing formal proofs on computers, based on each particular logical system.

我们开发了一种方法，它是逐步细化方法的扩展，用于使用指针操作和异常等高级特性的程序的正确性保持转换。我们已经说明，每个特性都有相应的逻辑系统，即指针操作的分离逻辑和异常的四值逻辑。已经证明，通过在计算机上基于每个特定的逻辑系统开发形式证明，程序的正确性得到了形式的保证。

项目成果

Algebraic Fusion of Functions with an Accumulating Parameter and its Improvement

带累加参数函数的代数融合及其改进

• 发表时间: 2006
• 期刊: ICFP'06: Proceedings of the 11th ACMSIGPLAN International Conference on Functional Programming
• 作者: Shin-ya Katsumata;Susumu Nishimura
• 通讯作者: Susumu Nishimura

Refining Exceptions in Four-Valued Logic

细化四值逻辑中的异常

• 发表时间: 2010
• 期刊: 19th International Symposium, LOPSTR 2009, Revised Selected Papers (Lecture Notes in Computer Science) vol.6037
• 作者: Toshiyuki Masuzawa;Yoshiyuki Uchishima;Takashi Fukui;Yoshihiro Okamoto;Maki Muto;Nobuo Koizumi;Akio Yamada;Susumu Nishimura
• 通讯作者: Susumu Nishimura

May & Must-Equivalence of Shared Variable Parallel Programs in Game Semantics

可能

• 发表时间: 2011
• 作者: Keisuke Watanabe;Susumu Nishimura
• 通讯作者: Susumu Nishimura

Refining Exception s in Four-Valued Logic

细化四值逻辑中的异常

• 发表时间: 2010
• 期刊: 19th Internatio nal Symposium, LOPSTR 2009, Revised Selected Papers
• 作者: A.M.S.Shrestha;S.Tayu;S.Ueno;長谷川真人;Susumu Nishimura
• 通讯作者: Susumu Nishimura

Safe Modification of Pointer Programs in Refinement Calculus

细化微积分中指针程序的安全修改

• 发表时间: 2009
• 作者: YamasakiS.;ShimamotoA.;TaharaH. and Okamoto T.;Akira Suzuki;Susumu Nishimura
• 通讯作者: Susumu Nishimura