対話型照明支援ツールPVSの紹介(<特集>続・システム検証の科学技術,サイバー増大号)

スポンサーリンク

概要

• 論文の詳細を見る

• 本論文の目的は,証明支援ツールの1つであるPVSおよびその応用例を紹介することである.第1節および第2節において,PVSおよびその作業の流れを大まかに説明する.第3節および第4節では,PVSにおける最も重要な概念である型および証明に関する説明を行う.第5節において,PVSの応用例として,特定の文字列を分類・変換する簡単なプログラムを取り上げ,PVSを用いてそのプログラムの検証を行う.

• 一般社団法人日本ソフトウェア科学会の論文
• 2005-07-26

著者

• 渡邊 宏

  産業技術総合研究所システム検証研究センター

• 高木 理

  京都産業大学理学部

• 渡邊 宏

  (独)産業技術総合研究所システム検証研究センター

• 武山 誠

  (独)産業技術総合研究所システム検証研究センター

関連論文

• 組み込みソフトウェア開発におけるモデル検査の適用事例(システム検証の科学技術)
• 画面遷移仕様のモデル検査(サイバー増大ページ論文概要,サイバー増大号)
• PVSを用いた遷移系簡約化の検証(サイバー増大ページ論文概要,サイバー増大号)
• 対話型照明支援ツールPVSの紹介(続・システム検証の科学技術,サイバー増大号)
• Representation of successor-type proof-theoretically regular ordinals via limits (Algebra, Languages and Computation)
• 超限的な再帰定義とBar帰納法を持つ構成的算術体系の自然演繹について

スポンサーリンク