文献

J-GLOBAL ID：202202275904243302   整理番号：22A1062871

マルチスレッドプログラム検証のための干渉関係誘導SMT解法【JST・京大機械翻訳】

Interference relation-guided SMT solving for multi-threaded program verification

著者 (3件)： Fan Hongyu (Tsinghua University, Beijing, China) ,  Liu Weiting (Tsinghua University, Beijing, China) ,  He Fei (Tsinghua University, Beijing, China)
資料名： ACM Proceedings  (ACM Proceedings)
号： PPoPP ’22  ページ： 163-176  発行年： 2022年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 同時プログラム検証は,多数のスレッド干渉のために困難である。ポピュラーなアプローチは,SMT公式として同時プログラムを符号化し,次に,検証を達成するために,オフショアのSMTソルバに依存することである。ほとんどの既存の研究において,SMTソルバはバックエンドとして簡単に処理される。同時プログラム検証のためにSMT解決を改善する研究はほとんどない。本論文では,マルチスレッドプログラムにおける干渉関係の特性を認識し,様々なメモリモデルの下でマルチスレッドプログラム検証のSMT解法における干渉関係を利用するための新しい方法を提案した。著者らは,バックエンドSMTソルバが同時プログラムのドメイン知識から大いに利益を得ることができることを示した。Zpreと呼ばれるプロトタイプツールに本手法を実装した。SV-COMP 2019のConcurrity Safetyカテゴリーから信頼できるベンチマークで最先端のZ3ツールと比較した。実験結果は,著者らのアプローチに起因する有望な改善を示した。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】

著者キーワード (5件)： 並行プログラム ,  半順序 ,  プログラム検証 ,  充足可能性モジュロ理論 ,  弱記憶モデル

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

タイトルに関連する用語 (6件)： マルチスレッド ,  プログラム検証 ,  干渉 ,  誘導 ,  SMT ,  解法