Actario: 定理証明支援系Coqによるアクターシステムの検証

安武祥平; 渡部卓雄

論文・著書情報

タイトル

和文:	Actario: 定理証明支援系Coqによるアクターシステムの検証
英文:

著者

和文:	安武祥平, 渡部卓雄.
英文:	Shohei Yasutake, Takuo Watanabe.

言語

Japanese

掲載誌/書名

和文:
英文:

巻, 号, ページ

出版年月

2016年3月7日

出版者

和文:
英文:

会議名称

和文:	日本ソフトウェア科学会第18回プログラミングおよびプログラミング言語ワークショップ(PPL 2016)
英文:

開催地

和文:	岡山県玉野市
英文:

公式リンク

http://logic.cs.tsukuba.ac.jp/ppl2016/

アブストラクト

アクターシステムの検証を目的とする，定理証明支援系CoqのライブラリActarioについて発表する．Actarioは以下のような特徴を持っている．(1)アクターモデルを使った並行アプリケーションをCoqのDSLを用いて記述できる．(2) アクターモデルの意味論を提供しており，アクターモデル自体の性質を検証できる．(3) 作成したアプリケーションに対してその性質を検証できる．(4) 作成したアプリケーションをErlangのコードに変換できる．本発表では，主にActarioで記述されたアプリケーションの検証手法について説明する．

Home

各種検索

サポート

T2R2について

関連リンク

論文・著書情報