関係検証のためのアラインメントの代数【JST・京大機械翻訳】

Antonopoulos Timos; Koskinen Eric; Le Ton Chanh; Nagasamudram Ramana; Naumann David A.; Ngo Minh

プレプリント

J-GLOBAL ID：202202200053708297 整理番号：22P0286890

関係検証のためのアラインメントの代数【JST・京大機械翻訳】

An algebra of alignment for relational verification

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (6件)： , , , , ,
資料名：
発行年： 2022年02月08日プレプリントサーバーでの情報更新日： 2023年03月23日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

※このプレプリント論文は学術誌に掲載済みです。なお、学術誌掲載の際には一部内容が変更されている可能性があります。

関係検証は,情報フローセキュリティ,回帰検証,コンパイラのための翻訳検証,およびより多くのものを含む。プログラムと計算の効果的なアラインメントは,より単純な関係不変量と関係手順の仕様の使用を促進し,次に自動化とモジュール推論を可能にする。アラインメントは,トレース対,関係Hoare論理(RHL)の演繹的規則,およびいくつかの形式の製品オートマトンに関して探索されてきた。本論文は,BiKATと呼ばれる試験(KAT)によるKleene Algebraの簡単な拡張が,すべての存在特性のためのアラインメントの wしさを含む事前定式化を,そのような特性のために軽い新しいRHLスタイル規則をもたらす,ということを示した。アラインメントは,アルゴリズム的に,または手動で考案できるが,いずれの場合も,元のプログラムに関するそれらの妥当性は証明されなければならない。明示的代数は,方程式推論によって建設的証明を可能にする。さらに,提案アプローチは,既存のKATベース技術とツールからアルゴリズム的利益を受け継ぎ,それは意味モデルの範囲に適用できる。【JST・京大機械翻訳】

, , , , , , , , , , , ,
, , , 【Automatic Indexing@JST】

計算機システム開発 , 計算理論

, ,

前のページに戻る