文献

J-GLOBAL ID：202002214768024402   整理番号：20A0267406

スパース行列計算の有界検証【JST・京大機械翻訳】

Bounded Verification of Sparse Matrix Computations

著者 (3件)： Dyer Tristan (North Carolina State University, USA) ,  Altuntas Alper (National Center for Atmospheric Research, USA) ,  Baugh John (North Carolina State University, USA)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2019  号： Correctness  ページ： 36-43  発行年： 2019年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 科学計算における多くの応用の中心であるスパース行列の構造と挙動についてのモデルと理由を示した。著者らのアプローチは,1つのモデルがもう一つの精密化であることを示すために,Alloyと呼ばれる形式に依存する状態ベースである。著者らは,疎行列ベクトル乗算,変換,およびELLPACKを用いたフォーマットと圧縮スパース列フォーマットとの間の変換の例を示し,このアプローチを実証した。Alloyのような宣言的言語における行列計算をモデル化するために,新しいidiomを増分更新による有界反復のために提示した。機械的検証は,ツールに組み込まれたSATソルバを用いて実行される。Copyright 2020 The Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 精密化 ,  モデリング ,  ベクトル ,  言語 ,  *スパース行列 ,  乗算
準シソーラス用語： ソルバ ,  *行列計算 ,  *有界 , 【Automatic Indexing@JST】

分類 (1件)： 図形・画像処理一般  (JE04010I)

タイトルに関連する用語 (4件)： スパース行列 ,  計算 ,  有界 ,  検証