Verification of Software with Interactive Theorem Proving
Verification of Software with Interactive Theorem Proving
用交互式定理证明验证软件
批准号：
18700018
负责人：
MINAMIDE Yasuhiko
金额：
$2.18万
依托单位：
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2006
资助国家：
日本
项目状态：
已结题
起止时间：
2006 至 2008
中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
対話的定理証明によるソフトウェアの検証について、様々な角度から研究を行い、事例研究を通じ、小規模なソフトウェアやソフトウェアの核となる部分については、対話的定理証明による検証が可能であることを示した。特に、本研究の代表者が開発しているウェブプログラムの検証ツールPHP文字列解析器について、その核となるアルゴリズムの定式化・検証を行い、正当性を検証済みのプログラムを得ることに成功した。
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
多相レコード型に基づくRubyプログラムの型推論
基于多态记录类型的 Ruby 程序类型推断
基于多态记录类型的 Ruby 程序类型推断
DOI：
--
发表时间：
2008
期刊：
情報処理学会論文誌:プログラミング 49
影响因子：
--
作者：
[中島浩, 小西昌裕, 中田尚, 松本宗太郎・南出靖彦]
通讯作者：
松本宗太郎・南出靖彦
ブラウザにおけるJavaScript 実行のモデル化
在浏览器中对 JavaScript 执行进行建模
在浏览器中对 JavaScript 执行进行建模
DOI：
--
发表时间：
2008
期刊：
影响因子：
--
作者：
[安田峰悠, 松本宗太郎, 南出靖彦]
通讯作者：
南出靖彦
ソフトウェア解説 : Cプログラムの検証ツール Caduceus
软件说明：C程序验证工具Caduceus
软件说明：C程序验证工具Caduceus
DOI：
--
发表时间：
2007
期刊：
コンピュータソフトウェア Vol.24, No.3
影响因子：
--
作者：
[松本, 宗太郎・南出, 靖彦, 南出靖彦]
通讯作者：
南出靖彦
Cプログラムの検証ツール Caduceus
C程序验证工具Caduceus
C程序验证工具Caduceus
DOI：
--
发表时间：
2007
期刊：
コンピュータコンピュータソフトウェア 24
影响因子：
--
作者：
[南出, 靖彦]
通讯作者：
靖彦
多相型レコードに基づくRubyオブジェクトの型推論に関する考察
基于多态记录的Ruby对象类型推断的思考
基于多态记录的Ruby对象类型推断的思考
DOI：
--
发表时间：
2006
期刊：
影响因子：
--
作者：
[松本宗太郎, 南出靖彦]
通讯作者：
南出靖彦
共 12 条
String Analysis for the Development of Web Software
-
批准号：24500028
-
项目类别：Grant-in-Aid for Scientific Research (C)
-
资助金额：$3.24万
-
财政年份：2012
-
负责人：MINAMIDE Yasuhiko
-
依托单位：
Verification of Web Software Based on String Analysis
-
批准号：21500028
-
项目类别：Grant-in-Aid for Scientific Research (C)
-
资助金额：$2.75万
-
财政年份：2009
-
负责人：MINAMIDE Yasuhiko
-
依托单位：
海外基金