文献

J-GLOBAL ID：202002232179745078   整理番号：20A0855294

単一パスHEAP操作プログラムのためのメモリ安全性の決定【JST・京大機械翻訳】

Deciding memory safety for single-pass heap-manipulating programs

著者 (5件)： Mathur Umang (University of Illinois at Urbana-Champaign, USA) ,  Murali Adithya (University of Illinois at Urbana-Champaign, USA) ,  Krogmeier Paul (University of Illinois at Urbana-Champaign, USA) ,  Madhusudan P. (University of Illinois at Urbana-Champaign, USA) ,  Viswanathan Mahesh (University of Illinois at Urbana-Champaign, USA)
資料名： Proceedings of the ACM on Programming Languages  (Proceedings of the ACM on Programming Languages)
巻： 4  号： POPL  ページ： 1-29  発行年： 2019年 
JST資料番号： W5683A  ISSN： 2475-1421  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： ここでは,ヒープを操作するプログラムに対する自動プログラム検証の決定可能性,特に,それらに対するメモリ安全性を証明するための決定手順を検討した。著者らは,マップを更新することができる一種のエイリアシングを意識したプログラムに対して,未解釈のプログラムの脱落可能なサブクラスを同定する最近の研究を拡張した。この理論を適用して,メモリ位置を割り当て,自由化し,ヒープポインタを操作することにより,非割り当てメモリ位置を参照しない場合に,メモリ安全性決定のための検証アルゴリズムを開発した。この問題は,最初に割り当てられたヒープが森林データ構造を形成し,プログラムがストリームコヒーレントである場合に決定可能であることを示した。これはプログラムがデータ構造上で単一パスを作るためにプログラムを直感的に制限する。森林データ構造を操作する一連のライブラリールーチンに関する著者らの実験評価は,データ構造に関する一般的な単一パスアルゴリズムがしばしば脱落可能なクラスに落ちることを示して,著者らの決定手順がそれらを検証することにおいて効率的であることを示した。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  ヒープ ,  エイリアシング ,  コヒーレンス ,  *記憶装置 ,  インタプリタ ,  ストリーミング ,  データ構造 ,  プログラム検証
準シソーラス用語： 実験評価 ,  ルーチン ,  ポインタ ,  決定可能性 , 【Automatic Indexing@JST】

著者キーワード (7件)： エイリアシング ,  決定可能性 ,  森林データ構造 ,  記憶の安全性 ,  プログラム検証 ,  ストリーミングコヒーレンス ,  未解釈プログラム

分類 (2件)： 言語プロセッサ  (JD03040F) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (2件)： パス ,  安全性