抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
フラッシュプロトコルは工業規模のキャッシュコヒーレンスプロトコルであり,形式的検証領域における挑戦的ベンチマークである。そのようなプロトコルを検証することは,科学的および商業的価値の両方をもたらす。しかし,プロトコルと爆発的探索状態の複雑な機構は,それを解決することを非常に困難にした。代替解決策は,この分野においてほとんどの研究によって採用されているコンピュータと人手作業を組み合わせたスクリプトを証明することである。しかし,この変更は検証プロセスを有効でも厳密でもない。そこで,本論文では,パラVerifierが形式的証明を自動的に生成する方法を詳細に述べた。それは手動作業なしで形式的証明を作り出すことができて,同時に厳密な正当性を保証した。さらに,FLASHプロトコルにおけるREADとWRITEトランザクションのフローチャートを例示し,自動探索不変量の背後にある意味論を解析した。パラVerifierは形式的証明を自動的に生成できるだけでなく,より良い理解のための包括的な解析報告を提供することを示した。Copyright 2018 The Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】
