RustMC: Extending the GenMC stateless model checker to Rust

• URL: http://arxiv.org/abs/2502.06293v1
• Date: Mon, 10 Feb 2025 09:33:24 GMT
• Title: RustMC: Extending the GenMC stateless model checker to Rust
• Authors: Oliver Pearce, Julien Lange, Dan O'Keeffe,
• Abstract summary: RustMC is a stateless model checker that enables verification of concurrent Rust programs.<n>This tool paper presents the key challenges we addressed to extend GenMC.
• Score: 0.2799243500184682
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [63.23120252801889]
  CRUST-Bench is a dataset of 100 C repositories, each paired with manually-written interfaces in safe Rust as well as test cases. We evaluate state-of-the-art large language models (LLMs) on this task and find that safe and idiomatic Rust generation is still a challenging problem. The best performing model, OpenAI o1, is able to solve only 15 tasks in a single-shot setting.
  arXiv  Detail & Related papers  (2025-04-21T17:33:33Z)
• RustMap: Towards Project-Scale C-to-Rust Migration via Program Analysis and LLM [13.584956125542396]
  Rust offers superior memory safety while maintaining C's high performance. Existing automated translation tools, such as C2Rust, may rely too much on syntactic, template-based translation. This paper introduces a novel dependency-guided and large language model (LLM)-based C-to-Rust translation approach, RustMap.
  arXiv  Detail & Related papers  (2025-03-22T11:57:45Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages. This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• C2SaferRust: Transforming C Projects into Safer Rust with NeuroSymbolic Techniques [16.111888466557144]
  We present C2SaferRust, a novel approach to translate C to Rust. We first use C2Rust to convert C code to non-idiomatic, unsafe Rust. We decompose the unsafe Rust code into slices that can be individually translated to safer Rust by an LLM. After processing each slice, we run end-to-end test cases to verify that the code still functions as expected.
  arXiv  Detail & Related papers  (2025-01-24T05:53:07Z)
• SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
  We propose SVTRv2, a CTC model that beats leading EDTRs in both accuracy and inference speed. SVTRv2 introduces novel upgrades to handle text irregularity and utilize linguistic context. We evaluate SVTRv2 in both standard and recent challenging benchmarks.
  arXiv  Detail & Related papers  (2024-11-24T14:21:35Z)
• A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries [2.359557447960552]
  Rust is frequently used to interoperate with other languages.<n>Miri is the only dynamic analysis tool that can validate applications against these models.<n>Miri does not support foreign functions, indicating that there may be a critical correctness gap across the Rust ecosystem.
  arXiv  Detail & Related papers  (2024-04-17T18:12:05Z)
• JailbreakBench: An Open Robustness Benchmark for Jailbreaking Large Language Models [123.66104233291065]
  Jailbreak attacks cause large language models (LLMs) to generate harmful, unethical, or otherwise objectionable content. evaluating these attacks presents a number of challenges, which the current collection of benchmarks and evaluation techniques do not adequately address. JailbreakBench is an open-sourced benchmark with the following components.
  arXiv  Detail & Related papers  (2024-03-28T02:44:02Z)
• CogCoM: Train Large Vision-Language Models Diving into Details through Chain of Manipulations [61.21923643289266]
  Chain of Manipulations is a mechanism that enables Vision-Language Models to solve problems step-by-step with evidence. After training, models can solve various visual problems by eliciting intrinsic manipulations (e.g., grounding, zoom in) actively without involving external tools. Our trained model, textbfCogCoM, achieves state-of-the-art performance across 9 benchmarks from 4 categories.
  arXiv  Detail & Related papers  (2024-02-06T18:43:48Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  We propose Chain of Code, a simple yet surprisingly effective extension that improves LM code-driven reasoning. The key idea is to encourage LMs to format semantic sub-tasks in a program as flexible pseudocode that the interpreter can explicitly catch.
  arXiv  Detail & Related papers  (2023-12-07T17:51:43Z)
• Fixing Rust Compilation Errors using LLMs [2.1781086368581932]
  The Rust programming language has established itself as a viable choice for low-level systems programming language over the traditional, unsafe alternatives like C/C++. This paper presents a tool called RustAssistant that leverages the emergent capabilities of Large Language Models (LLMs) to automatically suggest fixes for Rust compilation errors. RustAssistant is able to achieve an impressive peak accuracy of roughly 74% on real-world compilation errors in popular open-source Rust repositories.
  arXiv  Detail & Related papers  (2023-08-09T18:30:27Z)
• Exploring Continual Learning for Code Generation Models [80.78036093054855]
  Continual Learning (CL) is an important aspect that remains underexplored in the code domain. We introduce a benchmark called CodeTask-CL that covers a wide range of tasks, including code generation, translation, summarization, and refinement. We find that effective methods like Prompt Pooling (PP) suffer from catastrophic forgetting due to the unstable training of the prompt selection mechanism.
  arXiv  Detail & Related papers  (2023-07-05T16:58:39Z)
• CoCoMIC: Code Completion By Jointly Modeling In-file and Cross-file Context [82.88371379927112]
  We propose a framework that incorporates cross-file context to learn the in-file and cross-file context jointly on top of pretrained code LMs. CoCoMIC successfully improves the existing code LM with a 33.94% relative increase in exact match and a 28.69% relative increase in identifier matching for code completion when the cross-file context is provided.
  arXiv  Detail & Related papers  (2022-12-20T05:48:09Z)
• Learning Local and Global Temporal Contexts for Video Semantic Segmentation [80.01394521812969]
  Contextual information plays a core role for video semantic segmentation (VSS) This paper summarizes contexts for VSS in two-fold: local temporal contexts (LTC) and global temporal contexts (GTC) We propose a Coarse-to-Fine Feature Mining (CFFM) technique to learn a unified presentation of LTC.
  arXiv  Detail & Related papers  (2022-04-07T09:56:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.