文献

J-GLOBAL ID：201802231698074414   整理番号：18A1354461

候補ベース不変生成の実装と評価【JST・京大機械翻訳】

Implementing and Evaluating Candidate-Based Invariant Generation

著者 (5件)： Betts Adam (Department of Computing, Imperial College London, London, United Kingdom) ,  Chong Nathan (Department of Computing, Imperial College London, London, United Kingdom) ,  Deligiannis Pantazis (Department of Computing, Imperial College London, London, United Kingdom) ,  Donaldson Alastair F. (Department of Computing, Imperial College London, London, United Kingdom) ,  Ketema Jeroen (Department of Computing, Imperial College London, London, United Kingdom)
資料名： IEEE Transactions on Software Engineering  (IEEE Transactions on Software Engineering)
巻： 44  号： 7  ページ： 631-650  発行年： 2018年 
JST資料番号： D0480D  ISSN： 0098-5589  CODEN： IESEDJ  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 誘導不変量の発見は静的プログラム検証の心臓にある。現在,帰納的不変生成に対する多くの自動解は柔軟ではなく,あるクラスのプログラムに適用できるか,あるいは予測不可能である。これらの欠陥をある程度回避する自動技術は,候補に基づく不変生成であり,それにより,多数の候補不変量が推測され,次に,音響プログラム分析器を用いて帰納的または拒絶されることが証明される。本論文では,GPU上で実行するプログラムに対する静的チェッカー,GPUVerifyにおけるカンジダベース不変生成の適用について述べた。著者らは,多くのオープンソーススイートとベンダSDKから引き出されたループを含む383GPUプログラムのセットを研究した。この集合の中で,253のベンチマークは検証のためのループ不変量の提供を必要とする。著者らは,潜在的なプログラム不変量を推定するために安価な静的解析を用いて,これらのベンチマークを扱うためのGPUVerifyの不変生成能力を増分的に改善するために用いた方法論について述べた。また,候補生成に対するルールの有効性を調べるために用いた一連の実験を記述し,それらの一般性に基づくルール(候補不変量を生成する範囲),ヒット率(生成した候補が成立する程度),影響(一つの生成ルールの成功が別のルールにより生成される候補に依存する程度)を評価した。この方法は,カンジダベースの不変生成に興味を持つ他の研究者にとって有用な枠組みとして役立つと考えられる。GPUVerifyによって生成された候補は,253のプログラムの231を検証するのに役立つ。しかし,この精度の向上により,GPUVerifyは遅くなる。すなわち,生成されるより多くの候補,より多くの時間は,誘導不変量である決定に費やされる。このプロセスを高速化するために,誤った候補を迅速に拒否することを目的とした4つの過小近似プログラム解析と,これらの解析が順序または並列に実行できる枠組みを調べた。2つのプラットフォームを通して,WindowsとLinuxを実行して,著者らの結果は,これらの技術の最良の組合せが,著者らのベンチマークを通して,それぞれ93.58×(Windows)と48.34×(Linux)の最良の速度を示し,10.24×(Windows)と43.31×(Linux)の最悪の遅延を示すことを示した。この戦略を並列化することにより,全体的不変生成速度を1.27×(Windows)と1.11×(Linux)に改善し,91.18×(Windows)と44.60×(Linux)の良好な最良事例速度を維持し,重要なことに,最悪事例を3.15×(Windows)と3.17×(Linux)に劇的に低減することを見出した。Copyright 2018 The Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 予測 ,  音響 ,  近似法 ,  Candida ,  分析機器 ,  不変量 ,  プログラム検証 ,  *不変性 ,  高速化 ,  ベンチマーク ,  プログラム解析 ,  普遍性 ,  Windows ,  Linux
準シソーラス用語： 静的解析 , 【Automatic Indexing@JST】

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (3件)： 不変 ,  実装 ,  評価