パラモジュレーションによって検証されたヒープ定理証明器

STEWART Gordon; BERINGER Lennart; APPEL Andrew W.

文献

J-GLOBAL ID：201202232024700840 整理番号：12A1689810

パラモジュレーションによって検証されたヒープ定理証明器

Verified Heap Theorem Prover by Paramodulation

出版者サイト複写サービスで全文入手
高度な検索・分析はJDreamⅢで {{ this.onShowJLink("http://jdream3.com/lp/jglobal/index.html?docNo=12A1689810&from=J-GLOBAL&jstjournalNo=D0915A") }}

著者 (3件)： , ,
資料名：
巻： 47 号： 9 ページ： 3-14 発行年： 2012年09月
JST資料番号： D0915A ISSN： 0362-1340 資料種別：逐次刊行物 (A)
記事区分：原著論文発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

効率のために検査器から証明器を分離する事が必要である事を疑う人がいるかもしれないが,現代の証明支援はこの点まで進んでいる。この主張の証拠として,筆者らはヒープデータの形状特性についての推論用のデファクト標準である分離論理において必要とされる効率的マシン検証決定手続きVeriStarを提示した。筆者らの知る限り,VeriStarは実世界の操作的意味論に接続する分離論理用の初のマシン検証定理証明器である。VeriStarアーキテクチャは分離論理実装の詳細からシステムの健全性証明を分離するために分離論理インタフェイスと呼ばれる新規の分離論理の抽象を採用しており,そこでモジュール性を向上する。純粋関数型言語を用いて実装したVeriStarの性能は元のSmallfootの検査器の性能と比肩する。

, , , , , , , ,

計算機システム開発 , 論理代数

, ,

前のページに戻る