9 0 0 0 OA 定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-
- 著者
- アフェルト レナルド
- 雑誌
- 情報処理
- 巻号頁・発行日
- vol.55, no.5, pp.482-491, 2014-04-15
近年,定理証明支援系による成功が続いている:数学の証明の形式化,コンパイラやオペレーティングシステムの検証,などである.近年,定理証明支援系が数学とセキュアなコンピュータシステムの構築に欠かせないツールになってきており,本稿では,定理証明支援系による実例を紹介し,代表的な定理証明支援系Coqの基本的な使い方を説明する.
言及状況
Facebook (1 users, 1 posts)
アフェルト レナルド：定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-，情報処理，Vol.55，No.5，pp.482-491（2014）．
Facebook における性別
- male (1 / 100.00%)
はてなブックマーク (1 users, 2 posts)
アフェルト レナルド：定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-，情報処理，Vol.55，No.5，pp.482-491（2014）．
アフェルト レナルド：定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-，情報処理，Vol.55，No.5，pp.482-491（2014）．
Twitter (7 users, 7 posts, 0 favorites)
Coqは組み込み関係での需要があるのか。
検証コストめっちゃ高いって書いてあったりAirbusと共同研究とか書いてあるから、バグがあってはならないような用途向けって感じかな。
https://t.co/GkhNBco6QT
@sanjutsu_yu このへんにCoqでの同値関係の理屈書いてて、まあこれ自体は納得できるのですが実装がわからない https://t.co/EbmkFiz5Zb https://t.co/Mm91GteY7H
定理証明支援系 https://t.co/VFZc7js6hV
アフェルト レナルド：定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-，情報処理，Vol.55，No.5，pp.482-491（2014）． / “情報学広場：情報処理学会電子図書館” http://t.co/lrjb5NJsvD
収集済み URL リスト
- https://ipsj.ixsq.nii.ac.jp/ej/?action=pages_view_main&active_action=repository_view_main_item_detail&item_id=100796&item_no=1&page_id=13&block_id=8 (3)
- https://ipsj.ixsq.nii.ac.jp/ej/index.php?action=pages_view_main&active_action=repository_action_common_download&item_id=100796&item_no=1&attribute_id=1&file_no=1&page_id=13&block_id=8 (4)
- https://ipsj.ixsq.nii.ac.jp/ej/index.php?active_action=repository_view_main_item_detail&page_id=13&block_id=8&item_id=100796&item_no=1 (3)