文献

J-GLOBAL ID：202002266529960396   整理番号：20A0855212

未解釈プログラムの決定可能な検証【JST・京大機械翻訳】

Decidable verification of uninterpreted programs

著者 (3件)： Mathur Umang (University of Illinois at Urbana-Champaign, USA) ,  Madhusudan P. (University of Illinois at Urbana-Champaign, USA) ,  Viswanathan Mahesh (University of Illinois at Urbana-Champaign, USA)
資料名： Proceedings of the ACM on Programming Languages  (Proceedings of the ACM on Programming Languages)
巻： 3  号： POPL  ページ： 1-29  発行年： 2019年 
JST資料番号： W5683A  ISSN： 2475-1421  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： このプログラムを用いて,定数,関数および関係に対する解釈を与える任意のデータモデル上で動作する解釈されていないプログラムプログラムを完全に自動的に検証する問題を研究した。検証問題は,与えられたプログラムが,ループ不変量,契約などを提供することなく,最終状態に関する同等性を有する量子化フリーの式を用いて書かれたポスト条件を満たすかどうかについて述べた。この問題は一般的には決定できないことを示した。本論文の主な貢献は,決定可能な検証を許容するコヒーレントプログラムと呼ばれるプログラムのサブクラスであり,PSPACEにおいて決定できる。次にこのクラスのプログラムをk-コヒーレントであるk∈Nのクラスに拡張する。ここでk∈Nは,kゴースト変数とそれらをコヒーレントにする割当を追加することにより得られる。また,決定可能性の結果を再帰関数呼によりプログラムに拡張し,決定可能性を得るための制約がなぜ必要であるかを示すいくつかの非決定性結果を証明した。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】

著者キーワード (5件)： コヒーレンス ,  決定可能性 ,  プログラム検証 ,  ストリーミング合同閉包 ,  未解釈プログラム

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

タイトルに関連する用語 (2件)： 解釈プログラム ,  検証