文献

J-GLOBAL ID：202202284392594466   整理番号：22A0216608

モデル検査C++プログラム【JST・京大機械翻訳】

Model checking C++ programs

著者 (3件)： Monteiro Felipe R. (Federal University of Amazonas, Manaus, Brazil) ,  Gadelha Mikhail R. (Igalia, A Coruna, Spain) ,  Cordeiro Lucas C. (University of Manchester, Manchester, UK)
資料名： Software Testing, Verification & Reliability  (Software Testing, Verification & Reliability)
巻： 32  号： 1  ページ： e1793  発行年： 2022年 
JST資料番号： W0720A  ISSN： 0960-0833  CODEN： JTREET  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 過去30年間,CまたはC++のようなシステムプログラミング言語におけるメモリ安全性問題は,セキュリティ脆弱性の最も重要な情報源の1つである。しかし,C++プログラム検証の複雑性に対処するために,限られた成功でほんのわずかな試みしか存在しない。C++プログラムを検証するために,有界モデル検査(BMC)と充足可能性モジュロ理論(SMT)に基づく新しい検証手法を記述し,評価した。この検証手法は,C++プログラミング言語が,テンプレート,遺伝,多型,例外処理,および標準Template Libraryのような,SMTの様々な洗練された特徴に符号化することによって,有界C++プログラムを分析する。著者らは,一次論理の解読可能なフラグメントを用いて,著者らの形式的検証フレームワークの中でこれらの特徴を定式化し,次に最先端のSMTソルバがいかに効率的に処理できるかを示した。ESBMCのトップに著者らの検証アプローチを実行した。LLVMビットコードから直接C++プログラムをチェックするための最先端の検証者であるLLBMCとDIVINEに対するESBMCを比較した。実験結果は,ESBMCが広範囲のC++プログラムを扱うことができ,より高い数の正しい検証結果を提示することを示した。さらに,ESBMCを通信ドメインにおける商用C++アプリケーションに適用し,計算オーバーフロー誤差を成功裏に検出し,セキュリティ脆弱性を潜在的に導くことができた。Copyright 2022 Wiley Publishing Japan K.K. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 記憶装置 ,  言語 ,  情報源 ,  プログラミング言語 ,  通信 ,  応用プログラム ,  プログラム検証 ,  オーバフロー ,  定式化 ,  セキュリティ ,  *C++言語 ,  *モデル検査
準シソーラス用語： ソルバ ,  脆弱性 ,  複雑性 , 【Automatic Indexing@JST】

著者キーワード (5件)： C++ ,  記憶安全性 ,  モデル検査 ,  SMT ,  ソフトウェア検証

分類 (1件)： 汎用プログラミング言語  (JD03051H)

タイトルに関連する用語 (2件)： モデル検査 ,  C++