研究課題
前年度に提案した無限小プログラミングのための検証のフレームワークに基づいて無限小プログラムのホーア論理に基づく検証手法を提案し実装した．本実装は (1) バックエンドにおいて既存の自動定理証明器を拡張なしに用いることができるという点 (2) 既存研究でソフトウェアのための形式検証手法として提案された手法をそのまま用いることができる点に特徴がある．本研究は，ハイブリッドシステムの検証手法として無限小プログラミングの枠組みを利用するための重要なステップである．提案手法の理論的枠組と本実装に基づく実験結果を論文にまとめ，コンピュータを用いた検証に関する国際会議会議 (CAV) において発表した．また，前年度まで手続き型言語として定式化されていた無限小プログラミングをストリーム処理言語に拡張した言語（超準ストリーム言語）の基礎づけと検証の研究を行った．ストリームは電気信号等により近い表現を持つため，本研究によってハイブリッドシステムの開発現場で用いられている設計図に直接形式検証を適用することが将来的に可能になると期待される．理論的にも (1) 超準化されたストリームと連続的な信号との関係 (2) 超準ストリームプログラムの不動点意味論 (3) 連続的信号を演繹的な検証手法である型システムで検証するための手法といった興味深い展開が見られている．本研究の内容を論文にまとめ，プログラミング言語の原理に関する国際会議 (POPL) において発表した．
翌年度、交付申請を辞退するため、記入しない。
すべて 2013 2012 その他
すべて 雑誌論文 (3件) (うち査読あり 3件) 学会発表 (4件) 備考 (1件)
The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013)
巻: 40 ページ: 417--430
http://doi.acm.org/10.1145/2429069.2429120
The 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012
巻: 27 ページ: 1--20
http://doi.acm.org/10.1145/2384616.2384618
Computer Aided Verification (CAV) 2012, published from LNCS
巻: 6756 ページ: 462--477
10.1007/978-3-642-31424-7_34
http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/
