文献

J-GLOBAL ID：201802233278955292   整理番号：18A0353091

抽象で失われるもの:マルチスレッドプログラムにおける単調性【Powered by NICT】

Lost in abstraction: Monotonicity in multi-threaded programs

著者 (3件)： Kaiser Alexander (University of Oxford, United Kingdom) ,  Kroening Daniel (University of Oxford, United Kingdom) ,  Wahl Thomas (Northeastern University, Boston, United States)
資料名： Information and Computation  (Information and Computation)
巻： 252  ページ： 30-47  発行年： 2017年 
JST資料番号： D0449A  ISSN： 0890-5401  CODEN： INFCEC  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： コンカレントシステムにおける単調性は,大域的状態における,新しいプロセスは状態へ添加した場合,システム作用は実行可能なことを規定している。概念である天然かつ有用で各糸の記憶が有限ならば,走行糸の数が未知である時でも単調性はしばしば安全性特性の決定可能性を保証する。本論文では,モデル検査のための有限データ糸抽象は単調性とすることができることを示した:述語抽象単調ソフトウェアは非単調論理プログラムをもたらす可能性がある-単調性は抽象化で失われる。結果として,無限状態システムのための適切な確立された安全性照査アルゴリズムは適用不能になった。引抜きにおける単調性は回復し,安全性に影響を与えずにできるかを示した。overapproximationsによる単調性を施行し従来の方法を改善した。非有界糸モデルチェッカmonabsにおいて筆者らの解決策を実装し,多数の並行プログラムとアルゴリズム,述語抽象化は,既存のツールを超えて基本的にしばしばに適用した。Copyright 2018 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【Powered by NICT】

シソーラス用語： *安全性 ,  アルゴリズム ,  ソフトウェア ,  モデル検査 ,  非単調論理
準シソーラス用語： 述語抽象化 ,  有界 ,  述語 ,  決定可能性 ,  *単調性 , 【Automatic Indexing@JST】

著者キーワード (4件)： マルチスレッドソフトウエア ,  パラメータ化された検証 ,  単調性 ,  述語抽象化

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

タイトルに関連する用語 (3件)： 抽象 ,  マルチスレッド ,  単調性