論文の概要: Formal verification in Solidity and Move: insights from a comparative analysis

• arxiv url: http://arxiv.org/abs/2502.13929v1
• Date: Wed, 19 Feb 2025 18:06:01 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-20 13:57:52.484060
• Title: Formal verification in Solidity and Move: insights from a comparative analysis
• Title（参考訳）: 固体と移動の形式的検証--比較分析による考察
• Authors: Massimo Bartoletti, Silvia Crafa, Enrico Lipparini,
• Abstract要約: SolidityとMoveは、異なる設計と検証アプローチを備えた2つのコントラクト言語である。 本稿では,2つの言語が検証にどのように影響するか,また2つの言語に対する検証ツールの現状について検討する。 我々の調査は、CertoraとAptos Move Proverで実施された検証タスクのオープンデータセットによって支援されている。
• 参考スコア（独自算出の注目度）: 0.40964539027092906
• License:
• Abstract: Formal verification plays a crucial role in making smart contracts safer, being able to find bugs or to guarantee their absence, as well as checking whether the business logic is correctly implemented. For Solidity, even though there already exist several mature verification tools, the semantical quirks of the language can make verification quite hard in practice. Move, on the other hand, has been designed with security and verification in mind, and it has been accompanied since its early stages by a formal verification tool, the Move Prover. In this paper, we investigate through a comparative analysis: 1) how the different designs of the two contract languages impact verification, and 2) what is the state-of-the-art of verification tools for the two languages, and how do they compare on three paradigmatic use cases. Our investigation is supported by an open dataset of verification tasks performed in Certora and in the Aptos Move Prover.
• Abstract（参考訳）: 形式的検証は、スマートコントラクトをより安全にし、バグを見つけたり、不在を保証したり、ビジネスロジックが正しく実装されているかどうかを確認する上で重要な役割を担います。 Solidityには、すでに成熟した検証ツールがいくつか存在するが、言語の意味論は、実際に検証を非常に困難にすることができる。 一方Moveは、セキュリティと検証を念頭に設計されており、その初期段階から正式な検証ツールであるMove Proverが付属している。 本稿では,比較分析を通して考察する。 1)2つの契約言語の異なる設計が検証にどのように影響するか、そして 2) 2つの言語に対する検証ツールの現状と,3つのパラダイム的ユースケースとの比較について検討する。 我々の調査は、CertoraとAptos Move Proverで実施された検証タスクのオープンデータセットによって支援されている。

関連論文リスト

• A SAT-based approach to rigorous verification of Bayesian networks [13.489622701621698]
  ベイジアンネットワークに適した検証フレームワークを導入し,これらの欠点に対処する。 本フレームワークは,(1)ベイジアンネットワークをブール論理リテラルに変換する2段階のコンパイルおよび符号化スキームと,(2)これらのリテラルを活用して制約として符号化された様々なプロパティを検証する形式的検証クエリの2つの主要なコンポーネントから構成される。 検証手法の効率をベンチマークし、実世界のシナリオでその実用性を実証する。
  論文  参考訳（メタデータ） (2024-08-02T03:06:51Z)
• Large Language Models for Judicial Entity Extraction: A Comparative Study [0.0]
  本研究では,事例法文書におけるドメイン固有エンティティの同定における大規模言語モデルの適用について検討する。 この研究は、Large Language Model Meta AI 3、Mistral、Gemmaを含む最先端のLarge Language Modelアーキテクチャの性能を評価する。
  論文  参考訳（メタデータ） (2024-07-08T09:49:03Z)
• DELTA: Pre-train a Discriminative Encoder for Legal Case Retrieval via Structural Word Alignment [55.91429725404988]
  判例検索のための識別モデルであるDELTAを紹介する。 我々は浅層デコーダを利用して情報ボトルネックを作り、表現能力の向上を目指しています。 本手法は, 判例検索において, 既存の最先端手法よりも優れている。
  論文  参考訳（メタデータ） (2024-03-27T10:40:14Z)
• Enhancing Translation Validation of Compiler Transformations with Large Language Models [5.103162976634333]
  本稿では,Large Language Models (LLM) を翻訳検証に組み込むフレームワークを提案する。 まず,既存の形式検証ツールを用いて翻訳検証を行う。 フォーマルな検証ツールが変換の健全性を確認することができない場合、我々のフレームワークは予測に微調整のLLMを用いる。
  論文  参考訳（メタデータ） (2024-01-30T07:24:04Z)
• Do Language Models Learn about Legal Entity Types during Pretraining? [4.604003661048267]
  Llama2は特定のエンティティでよく機能し、最適化されたプロンプトテンプレートで大幅に改善する可能性を示す。 Llama2は、BERTベースのアーキテクチャでは欠点の少ない構文的ヒントをしばしば見落としているように見える。
  論文  参考訳（メタデータ） (2023-10-19T18:47:21Z)
• Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models [4.005483185111992]
  Trustworthiness Derivation Tree Analyzer (Trusta)は、TDTを自動構築し検証するデスクトップアプリケーションである。 バックエンドにはPrologインタプリタが内蔵されており、制約解決器Z3とMONAによってサポートされている。 Trustaは自然言語のテキストから形式的な制約を抽出し、解釈と検証を容易にする。
  論文  参考訳（メタデータ） (2023-09-22T15:42:43Z)
• Give Me More Details: Improving Fact-Checking with Latent Retrieval [58.706972228039604]
  証拠は、自動化された事実チェックにおいて重要な役割を果たす。 既存のファクトチェックシステムは、エビデンス文が与えられたと仮定するか、検索エンジンが返した検索スニペットを使用する。 資料から得られた全文を証拠として組み込んで,2つの豊富なデータセットを導入することを提案する。
  論文  参考訳（メタデータ） (2023-05-25T15:01:19Z)
• Towards Unsupervised Recognition of Token-level Semantic Differences in Related Documents [61.63208012250885]
  意味的差異をトークンレベルの回帰タスクとして認識する。 マスク付き言語モデルに依存する3つの教師なしアプローチについて検討する。 その結果,単語アライメントと文レベルのコントラスト学習に基づくアプローチは,ゴールドラベルと強い相関関係があることが示唆された。
  論文  参考訳（メタデータ） (2023-05-22T17:58:04Z)
• SAILER: Structure-aware Pre-trained Language Model for Legal Case Retrieval [75.05173891207214]
  判例検索は知的法体系において中心的な役割を果たす。 既存の言語モデルの多くは、異なる構造間の長距離依存関係を理解するのが難しい。 本稿では, LEgal ケース検索のための構造対応プレトランザクショナル言語モデルを提案する。
  論文  参考訳（メタデータ） (2023-04-22T10:47:01Z)
• DialFact: A Benchmark for Fact-Checking in Dialogue [56.63709206232572]
  われわれはDialFactという22,245の注釈付き会話クレームのベンチマークデータセットを構築し、ウィキペディアの証拠と組み合わせた。 FEVERのような非対話データでトレーニングされた既存のファクトチェックモデルは、我々のタスクでうまく機能しないことがわかった。 本稿では,対話におけるファクトチェック性能を効果的に向上する,シンプルなデータ効率のソリューションを提案する。
  論文  参考訳（メタデータ） (2021-10-15T17:34:35Z)
• Claim Check-Worthiness Detection as Positive Unlabelled Learning [53.24606510691877]
  クレームチェックの信頼性検出はファクトチェックシステムにおいて重要な要素である。 これらの課題の根底にあるクレームチェックの信頼性検出における中心的な課題を照明する。 我々の最良の手法は、正の非競合学習の変種を用いて、これを自動的に修正する統一的なアプローチである。
  論文  参考訳（メタデータ） (2020-03-05T16:06:07Z)

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

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