論文の概要: Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
- arxiv url: http://arxiv.org/abs/2409.02094v1
- Date: Tue, 3 Sep 2024 17:50:50 GMT
- ステータス: 処理完了
- システム内更新日: 2024-09-06 00:04:31.244447
- Title: Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
- Title（参考訳）: CPAchecker 3.0によるソフトウェア検証: チュートリアルとユーザガイド(拡張版)
- Authors: Daniel Baier, Dirk Beyer, Po-Chun Chien, Marie-Christine Jakobs, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch-Rosenfeld, Henrik Wachowitz, Philipp Wendler,
- Abstract要約: 本チュートリアルでは,CPAチェッカーの形式的ソフトウェア検証における基本的なユースケースについて述べる。
想定された読者は、自動形式検証とプログラム分析の背景を持っていると仮定される。
このチュートリアルとユーザガイドは、バージョン3.0のCPAチェッカーに基づいている。
- 参考スコア（独自算出の注目度）: 5.7013421104492075
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k -induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.
- Abstract（参考訳）: このチュートリアルでは、CPAcheckerをユーザに紹介する。
CPAcheckerは、ソフトウェア検証とテストのためのフレキシブルで構成可能なフレームワークである。
このフレームワークはBDD、明示的な値、インターバル、メモリグラフ、述語といった多くの抽象的なドメインを提供し、抽象的な解釈、境界モデルチェック、インパクト、補間ベースのモデルチェック、k-induction、PDR、述語抽象化、象徴的実行といった多くのプログラム分析とモデルチェックのアルゴリズムを提供している。
このチュートリアルでは、CPAチェッカーの基本的ユースケースを形式的ソフトウェア検証で紹介し、その長所と短所に焦点をあてる。
また、テストケース生成と証人ベースの結果検証のためのCPAチェッカーのさらなるユースケースを示す。
想定される読者は、自動形式検証とプログラム分析の背景を持っていると仮定されるが、CPAチェッカーの事前知識は必要ない。
このチュートリアルとユーザガイドは、バージョン3.0のCPAチェッカーに基づいている。
このユーザガイドの最新バージョンとドキュメントはhttps://cpachecker.sosy-lab.org/doc.php.comで公開されている。
関連論文リスト
- KAT: Dependency-aware Automated API Testing with Large Language Models [1.7264233311359707]
KAT(Katalon API Testing)は、APIを検証するためのテストケースを自律的に生成する、AI駆動の新たなアプローチである。
実世界の12のサービスを用いたKATの評価は、検証カバレッジを改善し、文書化されていないステータスコードを検出し、これらのサービスの偽陽性を低減できることを示している。
論文 参考訳（メタデータ） (2024-07-14T14:48:18Z) - Validating Traces of Distributed Programs Against TLA+ Specifications [0.0]
本稿では,分散プログラムのトレースをTLA+で記述した高レベル仕様に関連付けるためのフレームワークを提案する。
この問題は、TLCモデルチェッカーを用いて実現した制約付きモデルチェック問題に還元される。
提案手法を複数の分散プログラムに適用し,すべてのケースにおいて仕様と実装の相違を検出する。
論文 参考訳（メタデータ） (2024-04-24T01:33:07Z) - Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
機械学習の認証は、特定の条件下では、敵対的なサンプルが特定の範囲内でモデルを回避できないことを証明している。
セグメンテーションの一般的な認証方法は、平らな粒度のクラスを使い、モデルの不確実性による高い断続率をもたらす。
本稿では,複数レベルの階層内で画素を認証し,不安定なコンポーネントに対して粗いレベルに適応的に認証を緩和する,新しい,より実用的な設定を提案する。
論文 参考訳（メタデータ） (2024-02-13T11:59:43Z) - ConstraintChecker: A Plugin for Large Language Models to Reason on
Commonsense Knowledge Bases [53.29427395419317]
コモンセンス知識ベース(CSKB)に対する推論は,新しいコモンセンス知識を取得する方法として検討されてきた。
我々は**ConstraintChecker*を提案します。
論文 参考訳（メタデータ） (2024-01-25T08:03:38Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳（メタデータ） (2023-11-15T14:41:57Z) - A General Verification Framework for Dynamical and Control Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - LF-checker: Machine Learning Acceleration of Bounded Model Checking for
Concurrency Verification (Competition Contribution) [15.600922269515756]
機械学習に基づくメタ検証ツールLF-checkerを記述・評価する。
テスト中のプログラムの複数の特徴を抽出し、決定木による境界モデルチェッカーの最適構成を予測する。
論文 参考訳（メタデータ） (2023-01-22T15:46:57Z) - Plug and Play Counterfactual Text Generation for Model Robustness [12.517365153658028]
CASPerは、プラグアンドプレイのデファクト生成フレームワークである。
本稿では,CASPerが属性モデルによって提供されるステアリングに追従する反ファクトテキストを効果的に生成することを示す。
また,生成したデファクトをトレーニングデータの拡張に使用することにより,テストモデルをより堅牢にすることができることを示す。
論文 参考訳（メタデータ） (2022-06-21T14:25:21Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。
AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文 参考訳（メタデータ） (2021-09-25T22:53:24Z) - Beyond Accuracy: Behavioral Testing of NLP models with CheckList [66.42971817954806]
CheckList は NLP モデルをテストするためのタスクに依存しない方法論である。
CheckListには、包括的なテストのアイデアを促進する一般的な言語機能とテストタイプのマトリックスが含まれている。
ユーザスタディでは、CheckListのNLP実践者が2倍の数のテストを作成し、それのないユーザの約3倍のバグを発見しました。
論文 参考訳（メタデータ） (2020-05-08T15:48:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。