文献

J-GLOBAL ID：202202279084724959   整理番号：22A0777752

正規開発者にアクセス可能な浮動小数点プログラムの証明【JST・京大機械翻訳】

Making Proofs of Floating-Point Programs Accessible to Regular Developers

著者 (2件)： Dross Claire (AdaCore, Paris, France) ,  Kanig Johannes (AdaCore, Paris, France)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13124  ページ： 7-24  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 浮動点計算の形式的検証は,ソフトウェアエンジニアの課題として残っている。自動化,特殊化ツールは,浮動点計算をうまく扱うことができるが,他のタイプのデータまたは記憶推論と戦う。証明支援に基づく専門ツールは非常に強力であるが,高度な専門知識を必要とする。プログラムの演繹的検証のための汎用ツールは,近年,浮動点計算のためのサポートを追加したが,しばしば,証明された特性は,NaNまたはInfinityのような特別な値の範囲または不在の検証に限定されている。丸め誤差に対する限界のようなより複雑な特性の証明は,一般的に専門家に保存され,しばしば,バックエンドとして証明支援または特殊化ソルバのいずれかの使用を必要とする。本論文では,汎用SMTソルバに基づく一般的演繹検証ツールを用いて,丸め誤差に対する限界までの浮動点計算における異なる種類の特性を検証した。自動アクティブ検証に基づくアプローチを用いて,浮動点数を用いた加重平均の計算について実証を行った。SMTソルバーAlt-Ergo,CVC4,およびZ3に基づくAdaプログラムの形式的検証のために汎用ツールSPARKを使用するが,Frama-CまたはKeYのような他の類似言語とツールで原理的に実行することができる。Copyright Springer Nature Switzerland AG 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 誤差 ,  数値計算 ,  自動化 ,  言語 ,  浮動 ,  応用プログラム ,  *演繹 ,  システムエンジニア
準シソーラス用語： 加重平均 ,  バックエンド ,  形式的検証 ,  ソルバ ,  丸め誤差 , 【Automatic Indexing@JST】

著者キーワード (3件)： 演えき的検証 ,  数値計算 ,  数値精度

分類 (2件)： 演算方式  (JC02020Z) ,  数値計算  (JE02000J)

タイトルに関連する用語 (4件)： 開発 ,  アクセス ,  浮動小数点 ,  証明