論文の概要: Smart Contracts Formal Verification: A Systematic Literature Review
- arxiv url: http://arxiv.org/abs/2510.17865v1
- Date: Wed, 15 Oct 2025 21:32:57 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-25 03:08:12.233123
- Title: Smart Contracts Formal Verification: A Systematic Literature Review
- Title（参考訳）: スマートコントラクトの形式検証 - 体系的な文献レビュー
- Authors: Rene Davila, Everardo Barcenas, Rocio Aldeco-Perez,
- Abstract要約: 形式的検証は、指定された動作を保証するためにテストソフトウェアを必要とする。
ソフトウェアモデルとしてのスマートコントラクトは、しばしばオペレーションや仕様に顕著なエラーを含む。
本調査では,記述論理に基づく代替形式検証を提案する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: Formal verification entails testing software to ensure it operates as specified. Smart contracts are self-executing contracts with the terms of the agreement directly written into lines of code. They run on blockchain platforms and automatically enforce and execute the terms of an agreement when meeting predefined conditions. However, Smart Contracts, as software models, often contain notable errors in their operation or specifications. This observation prompts us to conduct a focused study examining related works published across various sources. These publications detail specifications, verification tools, and relevant experiments. Subsequently, this survey proposes an alternative formal verification based on description logic.
- Abstract（参考訳）: 形式的検証は、指定された動作を保証するためにテストソフトウェアを必要とする。
スマートコントラクトは,契約条件をコード行に直接記述した,自己実行型のコントラクトです。
ブロックチェーンプラットフォーム上で実行され、事前に定義された条件を満たすと、自動的に合意条件の強制と実行が行われる。
しかしながら、スマートコントラクトはソフトウェアモデルとして、オペレーションや仕様に顕著なエラーを含むことが多い。
この観察により,様々な資料にまたがる関連作品について,焦点を絞った調査を行うことが期待できる。
これらの出版物は仕様、検証ツール、関連する実験について詳述している。
そこで本研究では,記述論理に基づく代替形式検証を提案する。
関連論文リスト
- 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) - Vulnerabilities of smart contracts and mitigation schemes: A Comprehensive Survey [0.6554326244334866]
本稿では,開発者がセキュアなスマート技術を開発するのを支援することを目的とした,文献レビューと実験報告を組み合わせる。
頻繁な脆弱性とそれに対応する緩和ソリューションのリストを提供する。
サンプルのスマートコントラクト上でそれらを実行し、テストすることで、コミュニティが最も広く使用しているツールを評価します。
論文 参考訳（メタデータ） (2024-03-28T19:36:53Z) - Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
過去の取引履歴から契約仕様を推測するための仕様マイニング手法を提案する。
提案手法は,トランザクション履歴から統計的に推測されるプログラム不変量を伴って,関数呼び出しの高レベルな振る舞い自動を導出する。
SMCONは、高いコードカバレッジと最大56%のスピードアップを達成するためのスマートコントラクトのシンボリック分析を強化するために、合理的に正確な仕様をマイニングしている。
論文 参考訳（メタデータ） (2024-03-20T03:39:51Z) - Contract Usage and Evolution in Android Mobile Applications [45.44831696628473]
JavaやKotlinで記述されたAndroidアプリケーションにおけるコントラクトの存在と使用に関する,最初の大規模な実証的研究を紹介する。
F-Droidリポジトリから2,390のAndroidアプリケーションを解析し,51,749 KLOC以上を処理した。
私たちの発見は、JavaとKotlinでコントラクト仕様を標準化するライブラリを持つことが望ましいことを示しています。
論文 参考訳（メタデータ） (2024-01-25T15:36:49Z) - Formally Verifying a Real World Smart Contract [52.30656867727018]
われわれは、Solidityの最新バージョンで書かれた現実世界のスマートコントラクトを正式に検証できるツールを検索する。
本稿では,最近のSolidityで書かれた実世界のスマートコントラクトを正式に検証できるツールについて紹介する。
論文 参考訳（メタデータ） (2023-07-05T14:30:21Z) - Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。
使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
論文 参考訳（メタデータ） (2023-01-05T18:18:46Z) - ConReader: Exploring Implicit Relations in Contracts for Contract Clause
Extraction [84.0634340572349]
法律契約における暗黙の関係をモデル化し,契約条項の自動抽出(CCE)について検討する。
本研究ではまず,契約の複雑性問題を包括的に分析し,契約に共通する3つの暗黙の関係を抽出する。
本稿では,上記の3つの関係を利用して,より優れたコントラクト理解とCCEの改善を実現するための新しいフレームワークであるConReaderを提案する。
論文 参考訳（メタデータ） (2022-10-17T02:15:18Z) - Detecting Logical Relation In Contract Clauses [94.85352502638081]
契約における節間の論理的関係の抽出を自動化する手法を開発する。
結果として得られたアプローチは、コントラクト作者が節間の潜在的な論理的衝突を検出するのに役立つだろう。
論文 参考訳（メタデータ） (2021-11-02T19:26:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。