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. This tool paper presents the key challenges we addressed to extend GenMC.
• Score: 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.

Related papers

• 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)
• Towards Modified Condition/Decision Coverage of Rust [0.0]
  Modified Condition/Decision Coverage (MC/DC) is the highest software assurance level in aviation. Some central features of the Rust programming language necessitate further clarification. This paper informs the implementation of Rust MC/DC tools, paving the road towards Rust in high-assurance applications.
  arXiv  Detail & Related papers  (2024-09-13T10:53:32Z)
• VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners [6.824327908701066]
  Rust is a programming language that combines memory safety and low-level control, providing C-like performance. Existing work falls into two categories: rule-based and large language model (LLM)-based. We present VERT, a tool that can produce readable Rust transpilations with formal guarantees of correctness.
  arXiv  Detail & Related papers  (2024-04-29T16:45:03Z)
• A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries [2.359557447960552]
  Rust is frequently used to interoperate with other languages. Miri is the only dynamic analysis tool that can validate applications against these models. Miri does not support finding bugs in 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)
• 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.