文献

J-GLOBAL ID：202002258726225478   整理番号：20A2782011

SymPaths:記号実行は部分的次数削減に合致する【JST・京大機械翻訳】

SymPaths: Symbolic Execution Meets Partial Order Reduction

著者 (7件)： de Boer Frank S. (CWI, Amsterdam, The Netherlands) ,  Bonsangue Marcello (Leiden University, Leiden, The Netherlands) ,  Johnsen Einar Broch (Department of Informatics, University of Oslo, Oslo, Norway) ,  Pun Violet Ka I (Department of Informatics, University of Oslo, Oslo, Norway) ,  Pun Violet Ka I (Western Norway University of Applied Sciences, Bergen, Norway) ,  Tapia Tarifa S. Lizeth (Department of Informatics, University of Oslo, Oslo, Norway) ,  Tveito Lars (Department of Informatics, University of Oslo, Oslo, Norway)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 12345  ページ： 313-338  発行年： 2020年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 記号実行は,ソフトウェア解析のための重要な技術であり,与えられたプログラムのためのすべての可能な実行経路に従って,系統的モデル探査を可能にする。マルチスレッド共有可変プログラムのために,この技術は状態空間爆発をもたらす。部分次数低減は,等価実行経路を認識できる技術であり,状態空間爆発問題を低減する。本論文は,部分次数低減の使用の有無で,マルチスレッド共有可変プログラムのための記号実行の正当性と完全性を証明することによって,マルチスレッド設定におけるこれらの技術のための正式な正当化を提供した。次に,動的論理におけるそのようなマルチスレッド共有可変プログラムのための証明システムの健全性と相対完全性を証明するために,これらの形式的正当化がどのように実行するかを示し,部分次数低減を用いて状態空間爆発を緩和することによって証明構築を単純化できる。Copyright Springer Nature Switzerland AG 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 簡素化 ,  ソフトウェア ,  完全性 ,  *マルチスレッド ,  健全性
準シソーラス用語： 状態空間 , 【Automatic Indexing@JST】

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

タイトルに関連する用語 (2件)： 記号 ,  次数削減