@article{oai:ipsj.ixsq.nii.ac.jp:00100796,
 author = {アフェルト, レナルド and AFFELDT, Reynald},
 issue = {5},
 journal = {情報処理},
 month = {Apr},
 note = {近年，定理証明支援系による成功が続いている：数学の証明の形式化，コンパイラやオペレーティングシステムの検証，などである．近年，定理証明支援系が数学とセキュアなコンピュータシステムの構築に欠かせないツールになってきており，本稿では，定理証明支援系による実例を紹介し，代表的な定理証明支援系Coqの基本的な使い方を説明する．},
 pages = {482--491},
 title = {定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-},
 volume = {55},
 year = {2014}
}