日本語
 
Help Privacy Policy ポリシー/免責事項
  詳細検索ブラウズ

アイテム詳細

登録内容を編集ファイル形式で保存
 
 
ダウンロード電子メール
 タグ情報を表示リリース履歴を表示詳細要約
  Proving Thread Termination

Cook, B., Podelski, A., & Rybalchenko, A. (2007). Proving Thread Termination. In J., Ferrante, & K. S., McKinley (Eds.), PLDI'07: Proceedings of the 2007 Conference on Programming Language Design and Implementation (pp. 320-330). New York, NY, USA: ACM.

Item is

 

表示: 全項目 非表示: 全項目

基本情報

表示: 非表示:
アイテムのパーマリンク: https://hdl.handle.net/11858/00-001M-0000-000F-206B-F 版のパーマリンク: https://hdl.handle.net/11858/00-001M-0000-000F-206C-D
資料種別: 会議論文

ファイル

表示: ファイル
非表示: ファイル
:
Rybalchenko2007PLDI-Threads.pdf (全文テキスト（全般）), 5KB
 
ファイルのパーマリンク:
-
ファイル名:
Rybalchenko2007PLDI-Threads.pdf
説明:
-
OA-Status:
閲覧制限:
非公開
MIMEタイプ / チェックサム:
application/pdf
技術的なメタデータ:
著作権日付:
-
著作権情報:
-
CCライセンス:
-

関連URL

表示:

作成者

表示:
非表示:
 作成者:
Cook, Byron, 著者
Podelski, Andreas1, 著者           
Rybalchenko, Andrey1, 著者           
所属:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

内容説明

表示:
非表示:
キーワード: -
 要旨: Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Examples of such cases can be found in operating systems, web servers, e-mail clients, etc. Unfortunately, no known automatic program termination prover supports a practical method of proving the termination of threads. In this paper we describe such a procedure. The procedure's scalability is achieved through the use of environment models that abstract away the surrounding threads. The procedure's accuracy is due to a novel method of incrementally constructing environment abstractions. Our method finds the conditions that a thread requires of its environment in order to establish termination by looking at the conditions necessary to prove that certain paths through the thread represent well-founded relations if executed in isolation of the other threads. The paper gives a description of experimental results using an implementation of our procedureon Windows device drivers and adescription of a previously unknown bug found withthe tool.

資料詳細

表示:
非表示:
言語: eng - English
 日付: 2008-03-072007
 出版の状態: 出版
 ページ: -
 出版情報: New York, NY, USA : ACM
 目次: -
 査読: -
 識別子（DOI, ISBNなど）: eDoc: 356640
DOI: 10.1145/1250734.1250771
その他: Local-ID: C12573CC004A8E26-0E3286174490BE72C12572A2007E5F0F-Rybalchenko2007PLDI-Threads
 学位: -

関連イベント

表示:
非表示:
イベント名: Untitled Event
開催地: San Diego, CA, USA
開始日・終了日: 2007-06-10 - 2007-06-13

訴訟

表示:

Project information

表示:

出版物 1

表示:
非表示:
出版物名: PLDI'07 : Proceedings of the 2007 Conference on Programming Language Design and Implementation
種別: 会議論文集
 著者・編者:
Ferrante, Jeanne, 編集者
McKinley, Kathryn S., 編集者
所属:
-
出版社, 出版地: New York, NY, USA : ACM
ページ: - 巻号: - 通巻号: - 開始・終了ページ: 320 - 330 識別子（ISBN, ISSN, DOIなど）: ISBN: 978-1-59593-633-2