文献

J-GLOBAL ID：201702264504353712   整理番号：17A1774653

並列PDR設計【Powered by NICT】

Designing parallel PDR

著者 (4件)： Marescotti Matteo (Universita` della Svizzera italiana, Switzerland) ,  Gurfinkel Arie (University of Waterloo, Canada) ,  Hyvarinen Antti E. J. (Universita` della Svizzera italiana, Switzerland) ,  Sharygina Natasha (Universita` della Svizzera italiana, Switzerland)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： FMCAD  ページ： 156-163  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 特性指向型可到達性(PDR)は,効率的なモデル検査技術である。しかし,固有の高い計算の複雑さは,実世界検証の挑戦を満たすからPDRを防止する。この問題を解決するために,本論文では,に基づく並列アルゴリズムP3を紹介した。1)入力問題の分配,2)学習到達可能性情報の交換,および3)を用いてアルゴリズムポートフォリオ。提案した技術の包括的性質は直ちにソフトウェア検証に適したものにしている。本論文では,これらの技術の利点個々に行われたが一緒に組み合わせて,SMTソルバを使用するソフトウェアモデル検査器スペーサの上で分散コンピューティング環境を用いて実行した場合を調べた。SV COMPベンチマーク上での実験では,タイムアウトの中で解決多くの場合の2倍を用いた逐次実装に関して大きさ高速化の最大を観測した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： *モデル検査 ,  プログラム検証 ,  計算量 ,  分散処理 ,  スペーサ ,  並列アルゴリズム ,  ベンチマーク ,  学習 ,  ソフトウェア ,  高速化
準シソーラス用語： タイムアウト ,  ソルバ ,  モデル検査技術 , 【Automatic Indexing@JST】

分類 (2件)： 計算機網  (JC03000K) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (1件)： 設計