PPL2016 Poster

Posted on March 7, 2016

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

安武祥平,渡部卓雄
第18回プログラミングおよびプログラミング言語ワークショップ(PPL 2016), Mar. 7-9, 2016.

概要

アクターシステムの検証を目的とする,定理証明支援系CoqのライブラリActarioについて発表する.Actarioは以下のような特徴を持っている.

  1. アクターモデルを使った並行アプリケーションをCoqのDSLを用いて記述できる
  2. アクターモデルの意味論を提供しており,アクターモデル自体の性質を検証できる
  3. 作成したアプリケーションに対してその性質を検証できる
  4. 作成したアプリケーションをErlangのコードに変換できる

本発表では,主にActarioで記述されたアプリケーションの検証手法について説明する.