|
English Homepage : (→Click←)
高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証,
数学の形式化, および, 証明の計算機による検証に関する研究集会を
開催致します. 皆様のご参加をお待ちしています.
詳細は下記HPを参照下さい.
http://imi.kyushu-u.ac.jp/lasm/tpp2014/index_ja.html
招待講演者:
Adam Chlipala (MIT, USA),
「Correct-by-Construction Program Synthesis in Coq」
Cyril Cohen (INRIA Sophia-Antipolis, France),
「Mathematical Components and Algebraic Numbers」
栗田 太郎 (フェリカネットワークス),
「システム開発において数理論理学に基づいた仕様記述言語を用いることによる品質の確保」
今井 宣洋 (ITプランニング),
「Coqを使ったデジタルデータ放送におけるストリームデータ処理の形式化と検証」
矢田部 俊介 (JR西日本),
「コンセプト段階における準形式手法のシステム設計への利用」
阿原 一志 (明治大学),
「対話型幾何ソフトウエアと自動証明—シンデレラとキッズシンディ」
|
