論文の概要: Uma Prova de Conceito para a Verificação Formal de Contratos Inteligentes
- arxiv url: http://arxiv.org/abs/2601.14427v1
- Date: Tue, 20 Jan 2026 19:38:17 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-01-22 21:27:50.13204
- Title: Uma Prova de Conceito para a Verificação Formal de Contratos Inteligentes
- Title（参考訳）: インテリジェンテスの形式に就て : コンセト・パラとコンセト・パラ
- Authors: Murilo de Souza Neves, Adilson Luiz Bonifacio,
- Abstract要約: 本稿では、Relativized Contract Language(RCL)とRECALLツールを使って概念実証を行う。
この研究は、モデリングフェーズ中に規範的競合を検出するツールの能力を実証している。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Smart contracts are tools with self-execution capabilities that provide enhanced security compared to traditional contracts; however, their immutability makes post-deployment fault correction extremely complex, highlighting the need for a verification layer prior to this stage. Although formalisms such as Contract Language (CL) enable logical analyses, they prove limited in attributing responsibilities within complex multilateral scenarios. This work presents a proof of concept using the Relativized Contract Language (RCL) and the RECALL tool for the specification and verification of a purchase and sale contract involving multiple agents. The study demonstrates the tool's capability to detect normative conflicts during the modeling phase. After correcting logical inconsistencies, the contract was translated into Solidity and functionally validated within the Remix IDE environment, confirming that prior formal verification is fundamental to ensuring the reliability and security of the final code.
- Abstract（参考訳）: スマートコントラクトは、従来のコントラクトと比較してセキュリティを向上するセルフエグゼクティブ機能を備えたツールだが、その不変性は、デプロイ後の障害修正を極めて複雑にし、このステージ以前の検証レイヤの必要性を強調している。
契約言語(CL)のような形式主義は論理解析を可能にするが、複雑な多角的シナリオにおける責任の帰属は限定的である。
本稿では、複数のエージェントを含む購入販売契約の仕様と検証のために、RCL(Relativized Contract Language)とRECALLツールを用いて概念実証を行う。
この研究は、モデリングフェーズ中に規範的競合を検出するツールの能力を実証している。
論理的な矛盾を修正した後、契約はSolidityに変換され、Remix IDE環境内で機能的に検証された。
関連論文リスト
- Trace: Securing Smart Contract Repository Against Access Control Vulnerability [58.02691083789239]
GitHubはソースコード、ドキュメント、設定ファイルを含む多数のスマートコントラクトリポジトリをホストしている。
サードパーティの開発者は、カスタム開発中にこれらのリポジトリからコードを参照、再利用、フォークすることが多い。
スマートコントラクトの脆弱性を検出する既存のツールは、複雑なリポジトリを扱う能力に制限されている。
論文 参考訳（メタデータ） (2025-10-22T05:18:28Z) - Smart Contracts Formal Verification: A Systematic Literature Review [0.0]
形式的検証は、指定された動作を保証するためにテストソフトウェアを必要とする。
ソフトウェアモデルとしてのスマートコントラクトは、しばしばオペレーションや仕様に顕著なエラーを含む。
本調査では,記述論理に基づく代替形式検証を提案する。
論文 参考訳（メタデータ） (2025-10-15T21:32:57Z) - Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
PACTは、プログラムアセスメントおよび契約順応評価フレームワークである。
契約違反に焦点を当てた包括的なテストスーツコーパスを提供する。
様々なプロンプト条件下でのコード生成の体系的解析を可能にする。
論文 参考訳（メタデータ） (2025-10-14T01:12:37Z) - FaithCoT-Bench: Benchmarking Instance-Level Faithfulness of Chain-of-Thought Reasoning [62.452350134196934]
FaithCoT-Benchは、インスタンスレベルのCoT不信検出のための統一ベンチマークである。
我々の枠組みは差別的な決定問題として不誠実検出を定式化している。
FaithCoT-Bench は LLM のより解釈可能で信頼性の高い推論に向けた将来の研究の基盤となる。
論文 参考訳（メタデータ） (2025-10-05T05:16:54Z) - VulAgent: Hypothesis-Validation based Multi-Agent Vulnerability Detection [55.957275374847484]
VulAgentは仮説検証に基づくマルチエージェント脆弱性検出フレームワークである。
セマンティクスに敏感なマルチビュー検出パイプラインを実装しており、それぞれが特定の分析の観点から一致している。
平均して、VulAgentは全体的な精度を6.6%改善し、脆弱性のある固定されたコードペアの正確な識別率を最大450%向上させ、偽陽性率を約36%削減する。
論文 参考訳（メタデータ） (2025-09-15T02:25:38Z) - Validation Framework for E-Contract and Smart Contract [0.6312266245317322]
我々は,e-contractsから派生したスマートコントラクトを検証するためのフレームワークを提案し,開発する。
提案するフレームワークは,e-contractsの用語と節をスマートコントラクトの論理と体系的に比較し,検証する。
この検証により、合意が正確に実行可能なコードに変換されることを確認した。
論文 参考訳（メタデータ） (2025-04-27T07:23:46Z) - SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。
本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。
その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
論文 参考訳（メタデータ） (2025-03-03T01:55:20Z) - ContractTrace: Retracing Smart Contract Versions for Security Analyses [4.126275271359132]
ContractTraceは、スマートコントラクトのバージョンを正確に識別し、コヒーレントなラインにリンクする自動化インフラストラクチャです。
この機能は、脆弱性の伝播パターンを理解し、ブロックチェーン環境におけるセキュリティパッチの有効性を評価するために不可欠である。
論文 参考訳（メタデータ） (2024-12-30T11:10:22Z) - Formally Verifying a Real World Smart Contract [52.30656867727018]
われわれは、Solidityの最新バージョンで書かれた現実世界のスマートコントラクトを正式に検証できるツールを検索する。
本稿では,最近のSolidityで書かれた実世界のスマートコントラクトを正式に検証できるツールについて紹介する。
論文 参考訳（メタデータ） (2023-07-05T14:30:21Z) - Safety Verification of Declarative Smart Contracts [4.303272418564008]
本稿では,DeCon で記述された宣言型スマートコントラクトを対象とした自動安全検証ツール DCV を提案する。
20のベンチマークコントラクトに対する評価は,DCVがパブリックリポジトリから適応したスマートコントラクトの検証に有効であることを示し,他のツールがサポートしていないコントラクトの検証が可能であることを示唆している。
論文 参考訳（メタデータ） (2022-11-26T15:02:37Z) - Detecting Logical Relation In Contract Clauses [94.85352502638081]
契約における節間の論理的関係の抽出を自動化する手法を開発する。
結果として得られたアプローチは、コントラクト作者が節間の潜在的な論理的衝突を検出するのに役立つだろう。
論文 参考訳（メタデータ） (2021-11-02T19:26:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。