文献

J-GLOBAL ID：201602295399094065   整理番号：16A0811187

CEGARに基づくCプログラム空指針解検出を引用した。【JST・京大機械翻訳】

CEGAR Based Null-Pointer Dereference Checking in C Programs

著者 (3件)： Duan Zhao (Institute of Computing Theory and Technology, Xidian University) ,  Tian Cong (Institute of Computing Theory and Technology, Xidian University) ,  Duan Zhenhua (Institute of Computing Theory and Technology, Xidian University)
資料名： Jisuanji Yanjiu yu Fazhan  (Jisuanji Yanjiu yu Fazhan)
巻： 53  号： 1  ページ： 155-164  発行年： 2016年 
JST資料番号： W0790A  ISSN： 1000-1239  CODEN： JYYFEY  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： コンピュータソフトウェアの規模と複雑性の日々増加に伴い,ソフトウェアシステムの信頼性と安全性が注目されている。空指針解引用はプログラムにおける一般的な1種類のエラーである。空指針解検出方法を引用した1つの反例に基づく抽象精密化CEGAR誘導Cプログラムを提案した。この方法では,まず線形時相論理処理記述を用いて空指針解引用問題,次に被測定プログラムを抽象精密化の方法によって検出した中かどうか引用エラー空指針解を含有する。完全自動化検証の目標を達成するために,同時に空指針解引用問題,この類の性質を研究する論理の発現タイミングの方法に対して,そしてプログラムの中から,すべてのポインタ変数に対して,対応のタイミング論理式を自動生成する。実験の結果,提案の方法は大規模Cプログラムの空指針解引用検出において重要な実際的応用価値を持っている。Data from the ScienceChina, LCAS.【JST・京大機械翻訳】

シソーラス用語： 検出法 ,  信頼性 ,  安全性 ,  *精密化
準シソーラス用語： 自動生成 ,  論理式 ,  ポインタ ,  線形時間論理 ,  反例 ,  ソフトウェアシステム ,  複雑性 , 【Automatic Indexing@JST】

著者キーワード (5件)： model checking ,  abstraction refinement ,  null-pointer dereference ,  program verification ,  temporal logic

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (3件)： 指針 ,  解 ,  引用