抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
LIAMC,両整数モジュロ2~N(LIA_n)と整数(LIA)(量化記号無し)線形演算のための新しい決定方法を提示した。は広く使用されているLIA論理のための新しい効率的な決定手続きを設計する動機づけを説明するために必要ではない。LIA_n決定方法は,ソフトウェア(SW)検証のコンテキストの中で非常に有用である。SW検証は通常有限整数上の算術制約に関する推論する必要がある。この目的のために,現代のSW検証ツールは一般的に固定幅ビットベクトル(BV)ソルバを用いた。しかし,BVソルバの効率は劇的に低下幅は増加した。性能問題を解決するために,LIAソルバが適用されているが,それらは整数オーバーフローを扱うことができないので,不正確である。効率的なLIA_Nソルバは,この状況において理想的な解決策であると考えられる。決定手続きLIAMCは線形算術安全性検証への変換に基づいている。時間上でのビットの非有界ストリームとして整数を扱った。より正確には,各入力整数,最下位ビット(LSB)は,対応する河川における時間0に対応し,kビットは時間で受信したビットに対応する。LIAMCを用いて,得られた問題を解くためのSATベースモデルチェック(SATMC)を使用した。効率を達成するために,LIAMCは二型一般化を用いた。最初に,幅Nの充足不能であることを公式を発見した場合は,全ての幅に対してこの結果を一般化することを試みた。第二に,LIAMCは幅Nの満足であることを式を見つけたならば,それは「拡張」への試み,従って広い標的幅への帰属を一般化した。LIAMCを評価するために,SMT COMP’16のQF_LIAサブセットを用い,二組の実験を実行した。まず,著者らは種々の幅の固定幅ビットベクトル上のQF_LIAを再解釈とBoolectorとZ3の両方にLIAnモードにおけるLIAMCを比較した。LIAMCは最短幅32も三の最大充足可能インスタンスを解決した。第二に,元のQF_LIAベンチマーク上でCVC4及びZ3にLIAMCを比較した。LIAMCは他のソルバによる解決されていない多くの事例を解くことができた。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】
