Fugu-MT 論文翻訳(概要): RustMC: Extending the GenMC stateless model checker to Rust

論文の概要: RustMC: Extending the GenMC stateless model checker to Rust

arxiv url: http://arxiv.org/abs/2502.06293v1
Date: Mon, 10 Feb 2025 09:33:24 GMT
ステータス: 翻訳完了
システム内更新日: 2025-02-11 14:28:51.241692
Title: RustMC: Extending the GenMC stateless model checker to Rust
Title（参考訳）: RustMC: GenMCステートレスモデルチェッカーをRustに拡張
Authors: Oliver Pearce, Julien Lange, Dan O'Keeffe,
Abstract要約: RustMCは、並行するRustプログラムの検証を可能にするステートレスモデルチェッカーである。本ツールでは,GenMCの拡張に対処する上で重要な課題について述べる。
参考スコア（独自算出の注目度）: 0.2799243500184682
License:
Abstract: RustMC is a stateless model checker that enables verification of concurrent Rust programs. As both Rust and C/C++ compile to LLVM IR, RustMC builds on GenMC which provides a verification framework for LLVM IR. This enables the automatic verification of Rust code and any C/C++ dependencies. This tool paper presents the key challenges we addressed to extend GenMC. These challenges arise from Rust's unique compilation strategy and include intercepting threading operations, handling memory intrinsics and uninitialized accesses. Through case studies adapted from real-world programs, we demonstrate RustMC's effectiveness at finding concurrency bugs stemming from unsafe Rust code, FFI calls to C/C++, and incorrect use of atomic operations.
Abstract（参考訳）: RustMCは、並行するRustプログラムの検証を可能にするステートレスモデルチェッカーである。 RustとC/C++の両方がLLVM IRにコンパイルされるため、RustMCはLLVM IRの検証フレームワークを提供するGenMC上に構築されている。これにより、Rustコードと任意のC/C++依存関係の自動検証が可能になる。本ツールでは,GenMCの拡張に対処する上で重要な課題について述べる。これらの課題はRustのユニークなコンパイル戦略から生じ、スレッディング操作のインターセプト、メモリ固有の処理、初期化されていないアクセスなどが含まれる。実世界のプログラムから適応したケーススタディを通じて、安全でないRustコード、C/C++へのFFI呼び出し、原子操作の誤使用から発生する並行性バグを見つけるためのRustMCの有効性を実証する。

関連論文リスト

SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
CTCモデルであるSVTRv2を提案する。 SVTRv2は、テキストの不規則性に対処し、言語コンテキストを利用するための新しいアップグレードを導入した。我々は,SVTRv2を標準ベンチマークと最近のベンチマークの両方で評価した。
論文参考訳（メタデータ） (2024-11-24T14:21:35Z)
Translating C To Rust: Lessons from a User Study [12.49361031696427]
Rustは、未使用のCプログラムが楽しむことのない保証として、プログラムの完全なメモリ安全性を提供することを目指している。我々は,現実世界のCプログラムをRustに変換するよう人間に求めるユーザスタディについて報告する。私たちの参加者は安全なRust翻訳を作成できますが、最先端の自動ツールではそうできません。
論文参考訳（メタデータ） (2024-11-21T14:37:05Z)
Towards Modified Condition/Decision Coverage of Rust [0.0]
MC/DC (Modified Condition/Decision Coverage) は、航空業界で最も高いソフトウェア保証レベルである。 Rustプログラミング言語のいくつかの中心的な機能は、さらなる明確化を必要としている。本稿では,Rust MC/DCツールの実装について報告する。
論文参考訳（メタデータ） (2024-09-13T10:53:32Z)
VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners [6.824327908701066]
Rustはメモリ安全性と低レベルのコントロールを組み合わせたプログラミング言語で、Cライクなパフォーマンスを提供する。既存の作業はルールベースと大規模言語モデル(LLM)という2つのカテゴリに分類される。私たちは、正式な正確性を保証する形で、可読性のあるRustトランスパイルを生成するツールであるVERTを紹介します。
論文参考訳（メタデータ） (2024-04-29T16:45:03Z)
A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries [2.359557447960552]
Rustは、他の言語との相互運用に頻繁に使用される。 Miriは、これらのモデルに対してアプリケーションを検証できる唯一の動的解析ツールである。 Miriは外部機能をサポートしておらず、Rustエコシステムに重大な正当性ギャップがあることを示唆している。
論文参考訳（メタデータ） (2024-04-17T18:12:05Z)
JailbreakBench: An Open Robustness Benchmark for Jailbreaking Large Language Models [123.66104233291065]
ジェイルブレイク攻撃は、大きな言語モデル(LLM)が有害、非倫理的、またはその他の不快なコンテンツを生成する原因となる。これらの攻撃を評価することは、現在のベンチマークと評価テクニックの収集が適切に対処していない、多くの課題を提示します。 JailbreakBenchは、以下のコンポーネントを備えたオープンソースのベンチマークである。
論文参考訳（メタデータ） (2024-03-28T02:44:02Z)
Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
論文参考訳（メタデータ） (2023-12-07T17:51:43Z)
Fixing Rust Compilation Errors using LLMs [2.1781086368581932]
Rustプログラミング言語は、C/C++のような従来の安全でない代替言語よりも、低レベルのシステムプログラミング言語に実行可能な選択肢として、自らを確立している。本稿では,Large Language Models(LLMs)の創発的機能を活用し,Rustコンパイルエラーの修正を自動的に提案するRustAssistantというツールを提案する。 RustAssistantは、人気のあるオープンソースRustリポジトリの実際のコンパイルエラーに対して、約74%の驚くべきピーク精度を達成することができる。
論文参考訳（メタデータ） (2023-08-09T18:30:27Z)
Exploring Continual Learning for Code Generation Models [80.78036093054855]
継続的学習(CL)は、コードドメインの中でまだ過小評価されていない重要な側面である。コード生成,翻訳,要約,改良など,幅広いタスクをカバーするCodeTask-CLというベンチマークを導入する。即時選択機構の不安定な訓練により,プロンプトプール (PP) などの有効手法が破滅的な忘れ込みに悩まされることが判明した。
論文参考訳（メタデータ） (2023-07-05T16:58:39Z)
CoCoMIC: Code Completion By Jointly Modeling In-file and Cross-file Context [82.88371379927112]
予め訓練されたコード LM 上で,ファイル内コンテキストとファイル内コンテキストを協調的に学習するための,クロスファイルコンテキストを組み込んだフレームワークを提案する。 CoCoMICは既存のコードLMを33.94%の精度で改善し、クロスファイルコンテキストが提供されるとコード補完のための識別子マッチングが28.69%増加した。
論文参考訳（メタデータ） (2022-12-20T05:48:09Z)
Learning Local and Global Temporal Contexts for Video Semantic Segmentation [80.01394521812969]
コンテキスト情報はビデオセマンティックセグメンテーション(VSS)のコア役割を果たす本稿では,VSSの文脈を2つにまとめる:ローカル時間文脈(LTC)とグローバル時間文脈(GTC)。 LTCの統一表現を学習するためのCFFM手法を提案する。
論文参考訳（メタデータ） (2022-04-07T09:56:36Z)

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