文献

J-GLOBAL ID：201902290434546098   整理番号：19A1195109

演えき検証のための記憶モデルにおけるポインタ分析の利用【JST・京大機械翻訳】

Exploiting Pointer Analysis in Memory Models for Deductive Verification

著者 (6件)： Bouillaguet Quentin (CEA, LIST, Software Reliability Laboratory, Gif-sur-Yvette, France) ,  Bouillaguet Quentin (IRIF, University Paris Diderot and CNRS, Paris, France) ,  Bobot Francois (CEA, LIST, Software Reliability Laboratory, Gif-sur-Yvette, France) ,  Sighireanu Mihaela (IRIF, University Paris Diderot and CNRS, Paris, France) ,  Yakobowski Boris (CEA, LIST, Software Reliability Laboratory, Gif-sur-Yvette, France) ,  Yakobowski Boris (AdaCore, Paris, France)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 11388  ページ： 160-182  発行年： 2019年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 検証方法の間の協力は,ソフトウェア検証の挑戦的問題に取り組むために重要である。本論文では,ポインタを用いたCプログラムの検証に焦点を当て,ポインタ解析を行う静的解析器と一次論理に基づく演繹的検証ツールの間の協調を定式化した。ポインタ解析により推論されたメモリの分割を捕捉するメモリモデルに基づくフレームワークを提案し,検証条件を生成するために使用されるメモリモデルと比較した。このフレームワークは,ポインタ上の様々な低レベル操作に適応するポインタ解析を提案することを提案し,一方,演繹的検証に対するメモリ分割に関する正確な情報を提供した。Frama-Cプラットフォームの内部にこの協調を実装し,複雑な事例研究に関する演繹的検証のタスクを低減することにおけるその有効性を示した。Copyright 2019 Springer Nature Switzerland AG Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 定式化 ,  有効性 ,  事例研究 ,  プログラム検証 ,  記憶装置 ,  *演繹
準シソーラス用語： 静的解析 ,  *ポインタ , 【Automatic Indexing@JST】

分類 (4件)： 分子・遺伝情報処理  (JE15040B) ,  CAI  (JE09000G) ,  人工知能  (JE08000Z) ,  計算理論  (JB02000A)

タイトルに関連する用語 (4件)： 演えき ,  検証 ,  ポインタ ,  分析