Home >

news Help

Publication Information


Title
Japanese:Actario: 定理証明支援系Coqによるアクターシステムの検証 
English: 
Author
Japanese: 安武祥平, 渡部卓雄.  
English: Shohei Yasutake, Takuo Watanabe.  
Language Japanese 
Journal/Book name
Japanese: 
English: 
Volume, Number, Page        
Published date Mar. 7, 2016 
Publisher
Japanese: 
English: 
Conference name
Japanese:日本ソフトウェア科学会第18回プログラミングおよびプログラミング言語ワークショップ(PPL 2016) 
English: 
Conference site
Japanese:岡山県玉野市 
English: 
Official URL http://logic.cs.tsukuba.ac.jp/ppl2016/
 
Abstract アクターシステムの検証を目的とする，定理証明支援系CoqのライブラリActarioについて発表する．Actarioは以下のような特徴を持っている．(1)アクターモデルを使った並行アプリケーションをCoqのDSLを用いて記述できる．(2) アクターモデルの意味論を提供しており，アクターモデル自体の性質を検証できる．(3) 作成したアプリケーションに対してその性質を検証できる．(4) 作成したアプリケーションをErlangのコードに変換できる．本発表では，主にActarioで記述されたアプリケーションの検証手法について説明する．

©2007 Tokyo Institute of Technology All rights reserved.