研究課題
若手研究(B)
対話的定理証明によるソフトウェアの検証について、様々な角度から研究を行い、事例研究を通じ、小規模なソフトウェアやソフトウェアの核となる部分については、対話的定理証明による検証が可能であることを示した。特に、本研究の代表者が開発しているウェブプログラムの検証ツールPHP文字列解析器について、その核となるアルゴリズムの定式化・検証を行い、正当性を検証済みのプログラムを得ることに成功した。
すべて 2009 2008 2007 2006 その他
すべて 雑誌論文 (15件) (うち査読あり 12件) 学会発表 (4件) 備考 (1件)
InProc. POPL : The Symposium on Principles of Programming Languages
ページ: 200-212
Proc. POPL : The Symposium on Principle s of Programming Languages
Proc. of Symbolic Computation in Software Science Austrian-Japanese Workshop, RISC Technical Report 08-08
ページ: 137-147
In Proc. of the 13th International Conference on Implementation and Application of Automata LNCS 5148
ページ: 122-131
情報処理学会論文誌 : プログラミング Vol.49, No.SIG 3, PRO 36
ページ: 39-54
110006684629
Proc. of the 13th International Confer ence on Implementation and Application of Automata LNCS5148
情報処理学会論文誌:プログラミング 49
コンピュータソフトウェア Vol.24, No.3
ページ: 15-19
In Proc. of the 20th International Conference on Theorem Proving in Higher Order Logics LNCS 4732
ページ: 173-188
In Proc. of the Tenth International Conference on Foundations of Software Science and Computation Structures LNCS 4423
ページ: 346-3601
International Conference on Theorem Proving in Higher Order Logics LNCS 4732
コンピュータコンピュータソフトウェア 24
130004549074
Tenth International Conference on Foundations of Software Science and Computation Structures LNCS 4423
ページ: 346-360
In Proceedings of the Fourth Asian Symposium on Programming Languages and Systems (APLAS) LNCS 4279
ページ: 357-373
Fourth ASIAN Symposium on Programming Languages and Systems LNCS 4279
http://www.score.cs.tsukuba.ac.jp/~minamide/verification.html
