Wit4Java:Java検証者のための違反性検証者(競争貢献)【JST・京大機械翻訳】

Wu Tong; Schrammel Peter; Cordeiro Lucas C.

文献

J-GLOBAL ID：202202239216539746 整理番号：22A1105053

Wit4Java:Java検証者のための違反性検証者(競争貢献)【JST・京大機械翻訳】

Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)

出版者サイト複写サービスで全文入手 {{ this.onShowCLink("http://jdream3.com/copy/?sid=JGLOBAL&noSystem=1&documentNoArray=22A1105053&COPY=1") }}
高度な検索・分析はJDreamⅢで {{ this.onShowJLink("http://jdream3.com/lp/jglobal/index.html?docNo=22A1105053&from=J-GLOBAL&jstjournalNo=H0078D") }}

著者 (3件)： , ,
資料名：
巻： 13244 ページ： 484-489 発行年： 2022年
JST資料番号： H0078D ISSN： 0302-9743 資料種別：会議録 (C)
記事区分：原著論文発行国：ドイツ (DEU) 言語：英語 (EN)

著者らは,Wit4Javaと呼ばれるJava検証者のための,違反性検証者について説明し,評価する。Javaプログラムを,Java検証者による安全特性とそれぞれの違反-ness出出力を用いて,実行が特性に決定的に違反する新しいJavaプログラムを生成する。著者らは,違反性によって表される反例からプログラム変数の値を抽出して,この情報を元のプログラムにフィードバックした。さらに,著者らは,反例を注入することによって,ソースプログラムを具体化するための2つの実装を行った。実験結果は,Wit4Javaが数秒でJBMCとGDartによって作り出される違反度を正しく検証できることを示した。Copyright The Author(s) 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

, , , ,
, , 【Automatic Indexing@JST】

著者キーワード (3件)： , ,

計算機システム開発

, ,

前のページに戻る