文献

J-GLOBAL ID：202202211606079980   整理番号：22A0508003

巡回証明探索としてのソフトウェアモデル検査【JST・京大機械翻訳】

Software model-checking as cyclic-proof search

著者 (2件)： Tsukada Takeshi (Chiba University, Japan) ,  Unno Hiroshi (University of Tsukuba, Japan / RIKEN AIP, Japan)
資料名： Proceedings of the ACM on Programming Languages  (Proceedings of the ACM on Programming Languages)
巻： 6  号： POPL  ページ： 1-29  発行年： 2022年 
JST資料番号： W5683A  ISSN： 2475-1421  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 本論文は,様々なソフトウェアモデル検査アルゴリズムが,巡回証明システムとして知られる非標準証明システムのための証明研究戦略として見ることができることを示した。ソフトウェアモデル検査の論理的基礎としての循環証明システムの使用は,いくつかの簡単な原理からよく知られたアルゴリズムを再構成し,自由のためのアルゴリズムの健全性証明を得るために,異なるアルゴリズムを比較することができる。中でも,最大保守性と呼ぶ概念に基づく発見的方法の重要性を示した。これは,特性指向可到達性(PDR)のような重要なアルゴリズムのコアを説明し,一種のPDRと見なされない無限グラフ上のゲームの効率的なソルバへの驚くべき接続を明らかにした。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  ゲーム ,  発見的方法 ,  再構成 ,  *ソフトウェア ,  保全性 ,  *モデル検査 ,  健全性
準シソーラス用語： ソルバ ,  巡回 , 【Automatic Indexing@JST】

著者キーワード (4件)： 巡回証明システム ,  固定点論理 ,  特性指向可到達性 ,  ソフトウェアモデル検査

分類 (2件)： 計算機システム開発  (JD02010R) ,  論理代数  (JB03000H)

タイトルに関連する用語 (5件)： 巡回 ,  証明 ,  探索 ,  ソフトウェア ,  モデル検査