論文の概要: Formal Verification of Imperative First-Class Functions in Move

• arxiv url: http://arxiv.org/abs/2605.10007v1
• Date: Mon, 11 May 2026 05:31:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-12 23:28:50.547079
• Title: Formal Verification of Imperative First-Class Functions in Move
• Title（参考訳）: 運動における命令型第一級関数の形式的検証
• Authors: Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman,
• Abstract要約: Move Prover (MVP) は、Moveプログラミング言語で記述されたスマートコントラクトの形式検証である。 本稿では,Move仕様言語における関数値の表現とそのMVPにおける実装について述べる。
• 参考スコア（独自算出の注目度）: 2.6265820258267794
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. Recently, Move on Aptos was extended with higher-order functions: imperative functions as first-class values that can be passed around, stored in data structs, and kept in persistent storage, enabling dynamic dispatch. This paper describes the representation of function values in the Move specification language and their implementation in MVP. We introduce behavioral predicates which characterize Move functions (aborts and pre/post conditions) by single-state or two-state predicates. We also introduce state labels for naming intermediate memory states in which expressions are evaluated and which allow to compose behavioral predicates to describe sequences of state transitions. On SMT level, function values are encoded by discriminating over the possible function values reaching a call site: when the concrete function is known, its effect is accounted for directly; when it is unknown (for example, a function parameter, or a closure loaded from storage), its behavioral predicates describe the effect. Our approach goes beyond, for example, Dafny, by supporting imperative first-class functions which can modify state via Rust-style references and global variables, and leads to more efficient SMT encodings than separation logic because of the static separation of memory enabled by Move. We further extend MVP's specification inference tool to work with function values: given arbitrary higher-order Move code, weakest-precondition analysis semi-automatically derives behavioral-predicate-based specifications, reducing the annotation burden and providing a validation pipeline for the new specification constructs.
• Abstract（参考訳）: Move Prover (MVP) は、Moveプログラミング言語で記述されたスマートコントラクトの形式検証である。 最近、Move on Aptosは高階関数で拡張され、命令関数をファーストクラスの値として、渡したり、データ構造体に格納したり、永続的なストレージに保存したりすることで、動的ディスパッチを可能にした。 本稿では,Move仕様言語における関数値の表現とそのMVPにおける実装について述べる。 単状態または二状態の述語によってモーブ関数(吸収状態とポスト条件)を特徴づける行動述語を導入する。 また,表現が評価される中間記憶状態の命名のための状態ラベルを導入し,状態遷移のシーケンスを記述するための行動述語の作成を可能にする。 SMTレベルでは、関数値は呼び出しサイトに到達する可能性のある関数値を識別することで符号化される:具体的な関数が分かっている場合、その効果は直接説明される。 例えばDafnyは、Rustスタイルの参照とグローバル変数を通じて状態を変更可能な命令型ファーストクラスの関数をサポートし、Moveによって実現されたメモリの静的分離のため、分離ロジックよりも効率的なSMTエンコーディングを実現しています。 さらに、MVPの仕様推論ツールを関数値を扱うように拡張します。任意の高階モブ符号を与えられた場合、最弱条件解析は半自動で振る舞いに基づく仕様を導出し、アノテーションの負担を軽減し、新しい仕様構成のための検証パイプラインを提供します。

関連論文リスト

• Combining Mechanical and Agentic Specification Inference for Move [2.8693521708495684]
  本稿では,Move Proverの仕様推論ツールについて述べる。 これは、Moveバイトコードに対する最も弱い条件分析とClaude CodeのようなエージェントコーディングCLIを組み合わせる。 このツールは標準的なMoveコードのコーパスに適用されている。
  論文  参考訳（メタデータ） (2026-05-11T05:30:25Z)
• GUIDED: Granular Understanding via Identification, Detection, and Discrimination for Fine-Grained Open-Vocabulary Object Detection [54.19989440021701]
  細粒度オープン語彙オブジェクト検出(FG-OVD)は属性リッチテキストで記述された新しいオブジェクトカテゴリを検出することを目的としている。 FG-OVDは、非絡み合いモデリングとモジュラー最適化の利点を実証し、新しい最先端の結果を達成する。
  論文  参考訳（メタデータ） (2026-03-27T22:08:11Z)
• Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications [2.5164739639003364]
  よりリッチなデータタイプを操作するために、マイニング手順を拡張します。 我々は,OpenAI-Gymnasium ToyText環境上でのマイニング仕様からリアクティブプログラムを実演する。
  論文  参考訳（メタデータ） (2026-03-05T19:56:25Z)
• Mechanistic Knobs in LLMs: Retrieving and Steering High-Order Semantic Features via Sparse Autoencoders [8.188989044347595]
  意味論的に解釈可能な内部特徴の検索とステアリングのためのスパースオートエンコーダベースのフレームワークを提案する。 本研究では,ビッグファイブの性格特性をケーススタディとして用いて,モデル行動の正確かつ双方向なステアリングを可能にすることを実証する。
  論文  参考訳（メタデータ） (2026-01-06T12:40:37Z)
• Text2Mem: A Unified Memory Operation Language for Memory Operating System [59.082901444153684]
  モデルエージェントのための統一メモリ操作言語であるText2Memを紹介する。 Text2Memは、自然な正確性を保証するための標準化されたパスを提供する。
  論文  参考訳（メタデータ） (2025-09-14T07:30:09Z)
• IMoRe: Implicit Program-Guided Reasoning for Human Motion Q&A [25.91990824698619]
  本稿では,プログラム誘導型動作推論(IMoRe)フレームワークを提案する。 予め訓練されたモーション・ビジョン・トランス(ViT)から動的にマルチレベル・モーション・表現を選択するプログラム誘導型読み出し機構を導入する。 本モデルは,Babel-QA上での最先端性能を実現し,Hummanに基づく新たな動作Q&Aデータセットに一般化する。
  論文  参考訳（メタデータ） (2025-08-04T01:44:41Z)
• FIND: A Function Description Benchmark for Evaluating Interpretability Methods [86.80718559904854]
  本稿では,自動解釈可能性評価のためのベンチマークスイートであるFIND(Function Interpretation and Description)を紹介する。 FINDには、トレーニングされたニューラルネットワークのコンポーネントに似た機能と、私たちが生成しようとしている種類の記述が含まれています。 本研究では、事前訓練された言語モデルを用いて、自然言語とコードにおける関数の振る舞いの記述を生成する手法を評価する。
  論文  参考訳（メタデータ） (2023-09-07T17:47:26Z)
• First-Order Stable Model Semantics with Intensional Functions [2.1955512452222696]
  我々は、フェラーリス、リー、リフシッツによる一階安定モデル意味論を拡張して、インテンショナル函数を許容する。 ASPMT(Answer Set Programming Modulo Theories)の定義基盤としてこの拡張を使用します。 ASPMTは実数を含む領域に適用でき、基底問題を軽減することができる。
  論文  参考訳（メタデータ） (2023-07-15T06:03:35Z)
• Graph Adaptive Semantic Transfer for Cross-domain Sentiment Classification [68.06496970320595]
  クロスドメイン感情分類(CDSC)は、ソースドメインから学んだ伝達可能なセマンティクスを使用して、ラベルなしのターゲットドメインにおけるレビューの感情を予測することを目的としている。 本稿では、単語列と構文グラフの両方からドメイン不変セマンティクスを学習できる適応型構文グラフ埋め込み法であるグラフ適応意味伝達(GAST)モデルを提案する。
  論文  参考訳（メタデータ） (2022-05-18T07:47:01Z)
• Parameter-Efficient Tuning by Manipulating Hidden States of Pretrained Language Models For Classification Tasks [49.807185872741066]
  トレーニング可能なベクトルを3つだけ導入する簡単なチューニング手法を提案する。 統合された隠れ状態(s)をタスク固有の線形分類器に入力し、カテゴリを予測する。 このスキームは、ELMoが隠された状態をLSTMベースのモデルに供給する以外は、隠された状態を利用する方法に似ている。
  論文  参考訳（メタデータ） (2022-04-10T04:14:02Z)

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

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