WEKO3
-
RootNode
アイテム
定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-
https://ipsj.ixsq.nii.ac.jp/records/100796
https://ipsj.ixsq.nii.ac.jp/records/100796f00e7c4a-7bf2-4459-bfa0-8adf500f65e9
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-MGN550512 (793.2 kB)
|
Copyright (c) 2014 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Magazine(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2014-04-15 | |||||||
| タイトル | ||||||||
| タイトル | 定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門- | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Formal Verification using Proof-assistants – Survey of Recent Applications and Introduction to Coq - | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 解説 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | article | |||||||
| 著者所属 | ||||||||
| 産業技術総合研究所 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| National Institute of Advanced Industrial Science and Technology (AIST) | ||||||||
| 著者名 |
アフェルト, レナルド
× アフェルト, レナルド
|
|||||||
| 著者名(英) |
AFFELDT, Reynald
× AFFELDT, Reynald
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 近年，定理証明支援系による成功が続いている：数学の証明の形式化，コンパイラやオペレーティングシステムの検証，などである．近年，定理証明支援系が数学とセキュアなコンピュータシステムの構築に欠かせないツールになってきており，本稿では，定理証明支援系による実例を紹介し，代表的な定理証明支援系Coqの基本的な使い方を説明する． | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN00116625 | |||||||
| 書誌情報 |
情報処理 巻 55, 号 5, p. 482-491, 発行日 2014-04-15 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
