抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
テストベースの形式検証(TBFV)は,特定ベースのテストとHoare論理に基づくトラバースプログラム経路の正当性を検証するための厳密で潜在的に自動化されたアプローチであるが,Hoare論理が適用できないという事実のためにその能力は制限される。この挑戦に取り組むために,既存のTBFVにおけるHoare論理を置き換えるために記号実行を使用することを提案して,このように,TBFVの能力を強化した。新しく提案したアプローチTBFV-SE(TBFV-Symbolic Execation)と呼ぶ。既存のTBFVに対するTBFV-SEの利点は,完全自動化の特性を保存しながら,広範囲のプログラムへの適用性にある。ここでは,TBFV-SEの原理について述べ,2つの事例研究を提示し,その能力と有用性を実証した。また,TBFV-SEが効果的に使用できる条件とツールサポートの構築における潜在的課題について議論した。Copyright 2018 The Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】
