論文の概要: SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks

• arxiv url: http://arxiv.org/abs/2511.21509v1
• Date: Wed, 26 Nov 2025 15:44:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-27 18:37:59.172853
• Title: SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
• Title（参考訳）: SV-LIB 1.0: ソフトウェア検証タスクのための標準交換フォーマット
• Authors: Dirk Beyer, Gidon Ernst, Martin Jonáš, Marian Lingsch-Rosenfeld,
• Abstract要約: SV-LIBはソフトウェア検証タスクのための交換形式と中間言語である。 本稿では,SV-LIBformatのバージョン1.0について述べる。
• 参考スコア（独自算出の注目度）: 2.5374060352463697
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such asC, C++, and Java. Many of the used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIBis based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIBdefines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. This paper presents version 1.0 of the SV-LIBformat, including its design goals, the syntax, and informal semantics. Formal semantics and further extensions to concurrency are planned for future versions.
• Abstract（参考訳）: 過去20年間に、C、C++、Javaといった個々の言語に対する検証ツールの開発に重要な研究と開発が取り組んできた。 実際に使われている検証アプローチの多くは言語に依存しないものであり、他のプログラミング言語やモデリング言語にも実装を使用することは、技術移転にとって有益である。 そこで本研究では,プログラム,仕様,検証証人を含むソフトウェア検証タスクのための交換形式と中間言語であるSV-LIBを提案する。 SV-LIBisは命令型プログラミング言語からよく知られた概念に基づいており、SMT-LIBを使ってプログラムで使われる表現やソートを表現する。 これにより、多くの検証ツールがすでにSMTソルバをベースとしているため、既存のインフラストラクチャを解析し、組み込むのが容易になります。 さらに、SV-LIBは、正当かつ不正なSV-LIBプログラムの目撃者フォーマットと、証人検証タスクを特定する手段を規定する。 これにより、独立した証人バリデータの実装と、証人のバリデータとしても使える検証ツールの再利用が可能になる。 本稿では,SV-LIBformatのバージョン1.0について述べる。 形式的セマンティクスと並行性へのさらなる拡張は、将来のバージョンで計画されている。

関連論文リスト

• Evaluating Large Language Models for Code Translation: Effects of Prompt Language and Prompt Design [0.0]
  大規模言語モデル(LLM)はソースコードの自動翻訳を約束している。 しかし、モデル選択、迅速な設計、言語形翻訳の質に関する比較証拠は依然として限られている。 本研究は,C++,Java,Python,C#間のコード翻訳において,最先端のLLMを体系的に評価する。
  論文  参考訳（メタデータ） (2025-09-16T11:30:10Z)
• What Challenges Do Developers Face When Using Verification-Aware Programming Languages? [43.72088093637808]
  ソフトウェア開発では、ソフトウェア信頼性の増大はテストを伴うことが多い。 複雑でクリティカルなシステムでは、開発者はDesign by Contract(DbC)メソッドを使って、ソフトウェアコンポーネントが満たさなければならない正確な仕様を定義することができます。 VA(Verification-Aware)プログラミング言語は、DbCとコンパイル時または実行時の形式的検証をサポートし、従来のテストよりも正確性を保証する。
  論文  参考訳（メタデータ） (2025-06-30T10:17:39Z)
• Correctness Witnesses with Function Contracts [0.1499944454332829]
  我々は、関数契約の仕様化を可能にするために、既存の証人フォーマット2.0の拡張を提案する。 これにより、ツールからより多くの情報をエクスポートしたり、機能コントラクトを必要とするツールと情報を交換することが可能になる。
  論文  参考訳（メタデータ） (2025-01-21T17:27:59Z)
• SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
  テキストの不規則性や言語コンテキストのモデル化が可能なCTCモデルであるSVTRv2を提案する。 我々は,SVTRv2を標準ベンチマークと最近のベンチマークの両方で広範囲に評価した。 SVTRv2は精度と推論速度の点でほとんどのEDTRを超越している。
  論文  参考訳（メタデータ） (2024-11-24T14:21:35Z)
• AdaCCD: Adaptive Semantic Contrasts Discovery Based Cross Lingual Adaptation for Code Clone Detection [69.79627042058048]
  AdaCCDは、その言語でアノテーションを使わずに、新しい言語のクローンコードを検出する新しい言語間適応手法である。 5つのプログラミング言語からなる多言語コードクローン検出ベンチマークを構築し,AdaCCDの言語間適応性を評価する。
  論文  参考訳（メタデータ） (2023-11-13T12:20:48Z)
• Code Comment Inconsistency Detection with BERT and Longformer [9.378041196272878]
  ソースコードの自然言語記述であるコメントは、ソフトウェア開発者の間で標準的なプラクティスである。 コメントに付随する修正を加えずにコードを変更すると、コメントとコードの間に矛盾が生じます。 本研究では,自然言語推論(NLI)の文脈における不整合を検出するための2つのモデルを提案する。
  論文  参考訳（メタデータ） (2022-07-29T02:43:51Z)
• Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
  7つのテスト言語に対する並列データを持たないゼロショット問題として,言語間セマンティックパーシングについて検討した。 英文論理形式ペアデータのみを用いて解析知識を付加言語に転送するマルチタスクエンコーダデコーダモデルを提案する。 このシステムは、ゼロショット解析を潜時空間アライメント問題としてフレーム化し、事前訓練されたモデルを改善し、最小のクロスリンガル転送ペナルティで論理形式を生成することができる。
  論文  参考訳（メタデータ） (2021-04-15T16:08:43Z)
• VECO: Variable and Flexible Cross-lingual Pre-training for Language Understanding and Generation [77.82373082024934]
  我々はTransformerエンコーダにクロスアテンションモジュールを挿入し、言語間の相互依存を明確に構築する。 独自の言語でコンテキストにのみ条件付けされたマスク付き単語の予測の退化を効果的に回避することができる。 提案した言語間モデルでは,XTREMEベンチマークのさまざまな言語間理解タスクに対して,最先端の新たな結果が提供される。
  論文  参考訳（メタデータ） (2020-10-30T03:41:38Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。