論文の概要: A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets

• arxiv url: http://arxiv.org/abs/2604.02399v1
• Date: Thu, 02 Apr 2026 15:25:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-06 17:20:24.144524
• Title: A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets
• Title（参考訳）: プッシュダウン色付きペトリネットに基づく安全ラストコードの合成法
• Authors: Kaiwen Zhang, Guanjun Liu,
• Abstract要約: 本研究では,新たに定義されたPushdown Colored Net(PCPN)に基づく合成手法を提案する。 動的リソース状態を、借入が有効である寿命領域を示すスコープレベルと共に符号化する。 移行は、型マッチングとインターフェースの義務が保持され、必要なリソース状態が利用できる場合にのみ有効になる。
• 参考スコア（独自算出の注目度）: 5.064868362565062
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Safe Rust guarantees memory safety through strict compile-time constraints: ownership can be transferred, borrowing can temporarily guarantee either shared read-only or exclusive write access, and ownership and borrowing are scoped by lifetime. Automatically synthesizing correct and safe Rust code is challenging, as the generated code must not only satisfy ownership, borrowing, and lifetime constraints, but also meet type and interface requirements at compile time. This work proposes a synthesis method based on our newly defined Pushdown Colored Petri Net (PCPN) that models these compilation constraints directly from public API signatures to synthesize valid call sequences. Token colors encode dynamic resource states together with a scope level indicating the lifetime region in which a borrow is valid. The pushdown stack tracks the entering or leaving of lifetime parameter via pushing and popping tokens. A transition is enabled only when type matching and interface obligations both hold and the required resource states are available. Based on the bisimulation theory, we prove that the enabling and firing rules of PCPN are consistent with the compile-time check of these three constraints. We develop an automatic synthesis tool based on PCPN and the experimental results show that the synthesized codes are all correct.
• Abstract（参考訳）: 所有は転送可能で、借入は共有読み取り専用または排他的な書き込みアクセスを一時的に保証でき、所有と借入は生涯にわたってスコープ化される。 生成したコードはオーナシップ、借り出し、ライフタイムの制約を満足するだけでなく、コンパイル時に型とインターフェースの要件を満たす必要がある。 本研究では,新たに定義されたPushdown Colored Petri Net (PCPN) に基づいて,これらのコンパイル制約を公開APIシグネチャから直接モデル化し,有効なコールシーケンスを合成する合成手法を提案する。 動的リソース状態を、借入が有効である寿命領域を示すスコープレベルと共に符号化する。 プッシュダウンスタックは、プッシュとポップアップトークンを通じて、ライフタイムパラメータの入力または離脱を追跡する。 移行は、型マッチングとインターフェースの義務が保持され、必要なリソース状態が利用できる場合にのみ有効になる。 バイシミュレーション理論に基づき,PCPNの有効および発火規則は,これら3つの制約のコンパイル時チェックと一致していることを示す。 我々はPCPNをベースとした自動合成ツールを開発し, 実験結果から, 合成符号がすべて正しいことを示す。

関連論文リスト

• OrgForge: A Multi-Agent Simulation Framework for Verifiable Synthetic Corporate Corpora [0.0]
  本稿では,厳密な物理認識境界を強制するオープンソースのマルチエージェントシミュレーションフレームワークOrgForgeを紹介する。 アクターローカルクロックは、すべてのアーティファクトタイプにわたって因果タイムスタンプの正しさを強制する。 N日間のシミュレーションを実行すると、OrgForgeはインターリーブされたSlackスレッド、チケット、Confluenceページ、Gitのプルリクエスト、Eメールを生成する。
  論文  参考訳（メタデータ） (2026-03-16T09:02:24Z)
• TermiGen: High-Fidelity Environment and Robust Trajectory Synthesis for Terminal Agents [70.68963723787424]
  TermiGenは検証可能な環境とレジリエントな専門家軌道を合成するためのエンドツーエンドパイプラインである。 TermiGen-Qwen2.5-Coder-32B は TerminalBench 上で 31.3% のパスレートを達成した。
  論文  参考訳（メタデータ） (2026-02-06T23:56:50Z)
• SLICET5: Static Program Slicing using Language Models with Copy Mechanism and Constrained Decoding [13.61350801915956]
  静的プログラムスライシングはソフトウェア工学の基本的な技術である。 ourtoolは静的プログラムスライシングをシーケンス・ツー・シーケンスタスクとして再構成する新しいスライシングフレームワークである。 ourtoolは、最先端のベースラインを一貫して上回る。
  論文  参考訳（メタデータ） (2025-09-22T03:14:47Z)
• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
  CRUST-Benchは100のCリポジトリのデータセットで、それぞれが安全なRustとテストケースで手書きのインターフェースとペアリングされている。 我々は、このタスクで最先端の大規模言語モデル(LLM)を評価し、安全で慣用的なRust生成が依然として難しい問題であることを確認した。 最高のパフォーマンスモデルであるOpenAI o1は、ワンショット設定で15タスクしか解決できない。
  論文  参考訳（メタデータ） (2025-04-21T17:33:33Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• Improving Zero-Shot Generalization for CLIP with Synthesized Prompts [135.4317555866831]
  既存のほとんどのメソッドは、実世界のアプリケーションでは保持できない全てのクラスにラベル付きデータを必要とする。 既存の微調整法を改善するために,textbfSynttextbfHestextbfIzed textbfPrompts(textbfSHIP)と呼ばれるプラグアンドプレイ生成手法を提案する。
  論文  参考訳（メタデータ） (2023-07-14T15:15:45Z)
• Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification [151.62491805851107]
  私たちは、ニューロン毎の分割を完全にエンコードできるバウンド伝搬ベースの検証器である$beta$-crownを開発した。 Beta$-CROWNはLPベースのBaB法よりも3桁近い速さで堅牢性検証が可能です。 BaBを早期に終了することにより、不完全な検証にも使用できます。
  論文  参考訳（メタデータ） (2021-03-11T11:56:54Z)

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

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