Decision procedures of modal logics and their application to software verification

模态逻辑的决策过程及其在软件验证中的应用

• 批准号: 21500006
• 负责人: TANABE Yoshinori
• 金额: $ 1.75万
• 依托单位: National Institute of Informatics (2010-2011)The University of Tokyo (2009)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2009
• 资助国家: 日本
• 起止时间: 2009 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21500006/
• 关键词: 様相論理; 決定手続き; ソフトウェア検証; モデル検査; 充足可能性; 様相μ計算; min-plus代数; 法定手続き

We built a theory for applying modal logics to verification of programs that manipulate pointers, especially for techniques to judge the termination. It includes the weakest precondition and the strongest postcondition of operations of Kripke structures, and an extension of the semantics of modal mu-calculi. In the latter, we built a semantics in which truth values are members of min-plus algebra N-infty, and gave solutions to the model-checking problem and the satisfiability judgment problem with this semantics.

我们建立了一个理论，应用模态逻辑验证的程序，操作指针，特别是技术来判断终止。它包含了Kripke结构运算的最弱前置条件和最强后置条件，并扩展了模态μ演算的语义。在后者中，我们建立了一个真值是min-plus代数N-infty成员的语义，并给出了模型检验问题和可满足性判断问题的解决方案。

项目成果

Model checking distributed systems by combining caching and process checkpointing

• DOI: 10.1109/ase.2011.6100043
• 发表时间: 2011-11
• 期刊: 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)
• 作者: Watcharin Leungwattanakit;Cyrille Artho;M. Hagiya;Yoshinori Tanabe;M. Yamamoto

Toward Liveness Verification in Java Pathfinder

Java Pathfinder 中的活性验证

• 发表时间: 2009
• 作者: Yoshinori Tanabe;Vinh Cuong Tran;Masami Hagiya
• 通讯作者: Masami Hagiya

Decidability and Undecidability Results of Modalμ-calculi with N-infinity Semantics

具有 N 无穷大语义的模态 μ 演算的可判定性和不可判定性结果

• 发表时间: 2010
• 期刊: Proceedings of 17th Internaional Workshop of Logic, Language, Information and Computation(WoLLIC2010)
• 作者: Alexis Goyet;Masami Hagiya;Yoshinori Tanabe
• 通讯作者: Yoshinori Tanabe

Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications

• DOI: 10.1007/978-3-642-24690-6_24
• 发表时间: 2011-11
• 作者: K. Ono;Yoichi Hirai;Yoshinori Tanabe;N. Noda;M. Hagiya

ネットワークアプリケーションのマスター・スレーブ方式モデル検査アルゴリズムについて

关于网络应用的主从模型检查算法

• 发表时间: 2012
• 作者: 田辺良則;Cyriile Artho;Watcharin Leungwattanakit,山本光晴,萩谷昌己
• 通讯作者: Watcharin Leungwattanakit,山本光晴,萩谷昌己