Development of the Innovative Specification Verification System based on Proof Scores

基于证明分数的创新规格验证系统的开发

• 批准号: 23220002
• 负责人: FUTATSUGI Kokichi
• 金额: $ 111.74万
• 依托单位: Japan Advanced Institute of Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (S)
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011-04-01 至 2016-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23220002/
• 关键词: 仕様記述・仕様検証; 形式手法; ソフトウェア工学; 代数仕様; 証明スコア; CafeOBJ; 定理証明

项目成果

Foundations of Logic Programming in Hybridised Logics

混合逻辑中的逻辑编程基础

• DOI: 10.1007/978-3-319-28114-8_5
• 发表时间: 2015
• 期刊: Springer Lecture Notes in Computer Science (Recent Trends in Algebraic Development Techniques)
• 作者: Kazuhide Yasukata;Naoki Kobayashi;Kazutaka Matsuda;Daniel Gaina
• 通讯作者: Daniel Gaina

On Automation of OTS/CafeOBJ Method

OTS/CafeOBJ方法的自动化研究

• DOI: 10.1007/978-3-642-54624-2_29
• 发表时间: 2014
• 期刊: Specification, Algebra, and Software, LNCS, Springer
• 作者: Daniel Gaina;Dorel Lucanu;Kazuhiro Ogata;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi

Constructor-Based Inductive Theorem Prover

基于构造函数的归纳定理证明器

• DOI: 10.1007/978-3-642-40206-7_26
• 发表时间: 2013
• 期刊: Proc. of the 5th International Conference on Algebra and Coalgebra in Computer Science (5th CALCO), LNCS 8089, Springer
• 作者: Daniel Gaina;Min Zhang;Yuki Chiba;Yasuhito Arimoto
• 通讯作者: Yasuhito Arimoto

Formalization and Verification of Behavioral Correctness of Dynamic Software Updates

• DOI: 10.1016/j.entcs.2013.02.013
• 发表时间: 2013-03
• 作者: Min Zhang;K. Ogata;K. Futatsugi

Towards Formal Description of Standards for Automotive Operating Systems

• DOI: 10.1109/icstw.2013.8
• 发表时间: 2013-03
• 期刊: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops
• 作者: Hirokazu Yatsu;Takahiro Ando;W. Kong;K. Hisazumi;Akira Fukuda;Toshiaki Aoki;K. Futatsugi