| 研究課題/領域番号 |
25871113
|
|---|
| 研究機関 | 千葉工業大学 |
|---|
研究代表者 |
安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| キーワード | メモリ一貫性モデル / プログラム検証 / モデル検査 |
|---|
| 研究実績の概要 |
開発しているモデル検査器の有用性に関する論文(国際ワークショップ議事録)の執筆・発表は平成26年度までに終えていたため、平成27年度はそれの広報と実際のプログラミング言語の仕様書への適用を行った。具体的には、国際ワークショップ The 6th Workshop on Syntax and Semantics of Low-Level Languages において、本研究課題で行っている研究の概要を発表した。また、国産並列プログラミング言語 XcalableMP の仕様策定のワーキンググループに参加し、本研究課題で行った形式化されたメモリ一貫性モデルによる仕様記述の次期仕様書への採用を目指し、XcalableMP のメモリ一貫性モデルに関する章のドラフトの執筆を行った。また、主にアメリカで開発されている並列プログラミング言語 Chapel の開発者から仕様書に掲載しているプログラム例がメモリ一貫性モデルの観点から正しいかの確認を依頼されたため、これのフィードバックを行った。
また、メモリ一貫性モデルを考慮したプログラム検証において、正しさを保証するためのプログラム論理を構築できたため、それを使ってこれまでにプログラム論理で正しさを保証されていないプログラムを検証することができることを紹介する論文を執筆した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
研究実績の概要の最後に書いた論文の執筆について、採択までを平成27年度中に終える予定であったが、間に合わなかった。
|
| 今後の研究の推進方策 |
研究実績の概要の最後に書いた論文について、採択までを平成28年度中に終える予定である。
|
| 次年度使用額が生じた理由 |
国際会議向けに論文を執筆したが、投稿・採択までを平成27年度中に終えることができなかったため、その国際会議参加費用として計上していた予算に余りが生じた。
|
| 次年度使用額の使用計画 |
国際会議参加費用に充てる。
|
| 備考 |
本研究課題で実装した検査器を公開しているウェブページ。
|
