Awesome Rust Papers Explorer

Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought AKA: VCoT-Bench

ICML 2026 verification benchmarkLLMreasoning

PDF Code

Evaluating and Improving Automated Repository-Level Rust Issue Resolution with LLM-based Agents AKA: Rust-SWE-bench

ICSE 2026 ecosystem benchmarkLLMsoftware engineering

PDF Code

HarnessLLM: Rust Verification Harness Generation with Large Language Models AKA: HarnessLLM

ICSE 2026 verification harnessLLMMIR

PDF

Rusted Types: Static Detection of Rust Type Confusion Bugs AKA: DeRust

ICSE 2026 security type confusionstatic analysisdata-flow analysis

PDF Code

RusyFuzz: Unhandled Exception Guided Fuzzing for Rust OS Kernel AKA: RusyFuzz

ICSE 2026 security fuzzing panicoperating systemMIR

PDF

SmartC2Rust: Iterative, Feedback-Driven C-to-Rust Translation via Large Language Models for Safety and Equivalence AKA: SmartC2Rust

ICSE 2026 c2rust LLMmemory safety

PDF Code

From C to verifiable Rust: Towards practical migration of code and specifications AKA: C2VR

SCP 2026 c2rust verificationACSL

Hardening memory-safe languages: An empirical study of attack mitigations in rust and go binaries AKA: MitSBOM

Computers & Security 2026 security empirical studybinarymemory safetyhardeningSBOM

PyFgsea: a Rust-powered, fgseaMultilevel-aligned GSEA framework with rolling-window enrichment along single-cell trajectories AKA: PyFgsea

Bioinformatics 2026 product bioinformatics

Code

StarVerus: LLM-Powered Multi-Agent Collaboration for Industrial Rust Code Verification Automation AKA: StarVerus

SIGKDD 2026 verification proof generation LLMagentmulti-agent

PDF

&inator: Correct, Precise C-to-Rust Interface Translation AKA: &inator

PLDI 2026 c2rust interfaceLLVM IRSMT

PDF Code

A Comprehensive Empirical and Theoretical Analysis of Batching Algorithms for Efficient, Safe, Parallel Mutation Analysis in Rust

ACM TOSEM 2026 program analysis mutation analysisempirical study

PDF Code

A Deep Dive Into Deprecation Declarations in the Rust Package Ecosystem

IEEE TSE 2026 ecosystem deprecationempirical studydependency

A Mixed Methods Study on the Implications of Unsafe Rust for Interoperation, Encapsulation, and Tooling

ACM TOSEM 2026 ecosystem empirical studyunsafeFFIencapsulation

PDF

An Empirical Analysis of Rust Integration in Android Open Source Project

FSE Companion 2026 ecosystem Androidempirical studydocumentation

PDF

Auditing Rust Crates Effectively AKA: Cargo Scan

ESOP 2026 security static analysis dependencyempirical study

PDF Code

Beyond k-Limiting: Pointer-Flow-Guided Context Sensitivity for Scalable and Precise Rust Pointer Analysis AKA: Rceus

ECOOP 2026 program analysis pointer analysisstatic analysisRupta

PDF Code

C2SaferRust: Transforming C Projects Into Safer Rust With NeuroSymbolic Techniques AKA: C2SaferRust

IEEE TSE 2026 c2rust neuro symbolicLLMsafety

PDF Code

Clight2Rust: Translating a Subset of C into Safe Rust with a Small Trusted Runtime AKA: Clight2Rust

TASE 2026 c2rust borrow checker

CofferOS: Hardening OS-level Virtualization with Rust AKA: CofferOS

EuroSys 2026 product operating system virtualizationisolation

PDF Code

Cpp2Rust: Automatic Translation of C++ to Safe Rust AKA: Cpp2Rust

PLDI 2026 c2rust C++ownershipalias

PDF Code

deepSURF: Detecting Memory Safety Vulnerabilities in Rust Through Fuzzing LLM-Augmented Harnesses AKA: deepSURF

IEEE S&P 2026 security fuzzing harnessLLM

PDF Code

Dependency-Guided Repository-Level C-to-Rust Translation with Reinforcement Alignment AKA: DepTrans

FSE 2026 c2rust reinforcement learningLLMfine tune

PDF

Detecting Bugs in Rust Compiler Fix Suggestions via Constraint-Violation-Guided Mutation AKA: SugBreaker

FSE 2026 security compiler diagnosefuzzingborrow checkerlifetime

PDF

Enhancing LLM-Based Proof Synthesis for Rust Programs via Semantic Chunking and Hierarchical Context Expansion AKA: VERUSSEEK

TASE 2026 verification proof generation RAGLLMVerus

EvoC2Rust: A Skeleton-guided Framework for Project-Level C-to-Rust Translation AKA: EvoC2Rust

ICSE-SEIP 2026 c2rust LLMRAG

PDF Code

Formal Verification of a Rust-Based Buddy Physical Memory Allocator

TASE 2026 verification memory allocatoroperating system

Fortifying the Seams Between C/C++ and Rust: Characterizing Bugs in Interop Tools

ACM TOSEM 2026 ecosystem FFIempirical study

PDF Code

From Raw Pointers to Memory Safety: A Modular Demand-Driven Typestate Analysis for Rust AKA: Pincer

OOPSLA 2026 program analysis data-flow analysispointermemory safety

PDF Code

Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust AKA: Hayroll

PLDI 2026 c2rust preprocessorsymbolic executionmacro

PDF Code

Kani: A Model Checker for Rust AKA: Kani

arXiv 2026 verification model checkingMIR

PDF Code

MinsC2Rust: LLM-driven project-level code migration from C to safe Rust AKA: MinsC2Rust

Empirical Software Engineering 2026 c2rust LLM

Miri: Practical Undefined Behavior Detection for Rust AKA: Miri

POPL 2026 security soundnessundefined behavior

PDF Code

Oxidizer: Toward Concise and High-fidelity Rust Decompilation AKA: Oxidizer

IEEE S&P 2026 security decompilerbinary

PDF Code

PanicFI: An Infrastructure for Fixing Panic Bugs in Real-World Rust Programs AKA: PanicFI

ACM TOSEM 2026 program analysis panicbenchmarkpatchHIR

PDF

Project-Level C-to-Rust Translation via Pointer Knowledge Graphs AKA: PtrTrans

FSE 2026 c2rust LLMpointerunsafe

PDF Code

Raw Pointer Rewriting with LLMs for Translating C to Safer Rust AKA: PR2

ACL Findings 2026 c2rust LLMpointerdecision-tree

PDF Code

Ruby: Unmasking Unsafe Rust in Stripped Binaries via Machine Learning AKA: Ruby

DSN 2026 security binaryunsafemachine learning

PDF

RustC4++: Improving Rust Code-Comment Inconsistency Detection via Hybrid LLM and Static Analysis AKA: RustC4++

ACM TOSEM 2026 program analysis documentation code-comment inconsistencyLLMtraitSMT

PDF

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust AKA: RustCompCert

arXiv 2026 verification compilermemory safety

PDF

RUSTMC: Automated Verification of Real-World Concurrent Rust AKA: RUSTMC

FORTE 2026 verification concurrencyLLVM IRFFImodel checker

RustyDL: A Program Logic for Rust AKA: RustyDL

FM 2026 formalization human-in-the-loop

PDF Code

SACTOR: LLM-Driven Correct and Idiomatic C to Rust Translation with Static Analysis and FFI-Based Verification AKA: SACTOR

ACL 2026 c2rust LLMFFIpointer

PDF Code

Scylla: Translating an Applicative Subset of C to Safe Rust AKA: Scylla

OOPSLA 2026 c2rust pointerformalization

PDF Code

Two Birds One Stone: Effective Static Detection of Resource and Communication Deadlocks in Rust Programs AKA: RcChecker

Automated Software Engineering 2026 security concurrency deadlock

PDF

Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust

CPP 2026 verification ghostinterior mutabilityVerus

PDF Code

Verifying the Rust Standard Library AKA: verify-rust-std

NFM 2026 verification

PDF Code

VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System AKA: VerusBelt

PLDI 2026 verification type systemsoundnesslifetimeconcurrencyVerus

PDF Code

Automated Proof Generation for Rust Code via Self-Evolution AKA: SAFE

ICLR 2025 verification proof generation LLMself-evolutionfine tune

PDF

A systematic exploration of C-to-rust code translation based on large language models: prompt strategies and automated repair AKA: RustFlow

Automated Software Engineering 2025 c2rust LLMvalidation

Detecting Memory Errors in Rust Programs Including Unsafe Foreign Code AKA: CREMA

SEFM 2025 security memory safetystatic analysisFFI

Code

Drinking From a Firehose While Herding Cats: A Search for Accountability in the Rust Open Source Community

CSCW 2025 ecosystem accountabilityroadmap

PDF

Fuzzing trusted execution environments with Rust

Computers & Security 2025 product fuzzingTEEspecificationQEMU

Rust-doctor: Enhanced Feature for Rust Ownership and Lifetime Repair with Balanced Training Data Generation AKA: Rust-doctor

EMNLP 2025 security patch fine tunemachine learning

PDF

SBD: Securing safe rust automatically from unsafe rust AKA: SBD

SCP 2025 security isolation data-flow analysisMIR

PDF

Thetis-lathe: Guidance on Reducing Residual Safety Obstacle in System Software from Rust Source Codes AKA: Thetis-lathe

TECS 2025 program analysis unsafeunsafe reduction

PDF

Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust

NFM 2025 product embeddedverificationVerus

Unlocking a New Rust Programming Experience: Fast and Slow Thinking with LLMs to Conquer Undefined Behaviors AKA: RustBrain

DAC 2025 security patch LLMsoundness

PDF

A First Look at ROS 2 Applications Written in Asynchronous Rust

ECRTS 2025 product asynchronousrobotoperating system

PDF Code

A Hybrid Approach to Semi-Automated Rust Verification AKA: Gillian-Rust

PLDI 2025 verification proof generation type safetycorrectness

PDF Code

A Refinement Methodology for Distributed Programs in Rust

OOPSLA 2025 verification refinementinvariantdistributedonwership

PDF Code

A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries AKA: MiriLLI

ICSE 2025 security FFIsoundnessMiritree borrowempirical study

PDF Code

A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SEABMC AKA: SeaBMC

FMCAD 2025 verification LLVM IRunsafemodel checkerSMTpanic

PDF Code

An Empirical Study of Bugs in the rustc Compiler

OOPSLA 2025 ecosystem empirical studycompilerHIRMIR

PDF Code

An Interactive Debugger for Rust Trait Errors AKA: Argus

PLDI 2025 language debugtraittype inference

PDF Code

ASTERINAS: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCB AKA: ASTERINAS

USENIX ATC 2025 product operating system framekernel

PDF Code

Atmosphere: Practical Verified Kernels with Rust and Verus AKA: Atmosphere

SOSP 2025 product operating system verificationVerusmicrokernelcorrectness

PDF Code

Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials AKA: RaRust

OOPSLA 2025 program analysis performancestatic analysisresource consumptionborrow checker

PDF Code

AutoVerus: Automated Proof Generation for Rust Code AKA: AutoVerus

OOPSLA 2025 verification proof generation LLMAgentVeruscorrectness

PDF Code

Carapace: Static-Dynamic Information Flow Control in Rust AKA: Carapace

OOPSLA 2025 program analysis information flow controlsecrecyintegrity

PDF Code

Charon: An Analysis Framework for Rust AKA: Charon

CAV 2025 program analysis MIRAST

PDF Code

Clozemaster: Fuzzing Rust Compiler by Harnessing LLMs for Infilling Masked Real Programs AKA: Clozemaster

ICSE 2025 security compiler compilerLLMharnessfuzzing

PDF Code

Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness AKA: RUXt

ECOOP 2025 formalization undefined behaviorsoundness

PDF Code

Converos: Practical Model Checking for Verifying Rust OS Kernel Concurrency AKA: Converos

USENIX ATC 2025 verification model checkingconcurrencyPlusCal

PDF

Core Developer Turnover in the Rust Package Ecosystem: Prevalence, Impact, and Awareness

FSE 2025 ecosystem empirical studydeveloper turnover

PDF

CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation AKA: CRUST-Bench

arXiv 2025 c2rust empirical studybenchmark

PDF Code

Don't Panic! Finding Bugs Hidden Behind Rust Runtime Safety Checks AKA: PanicKiller

CCS 2025 security fuzzing panictaint analysisLLVM IR

PDF

Forcrat: Automatic I/O API Translation from C to Rust via Origin and Capability Analysis AKA: Forcrat

ASE 2025 c2rust I/OMIR

PDF Code

Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust

CCS 2025 verification cryptographic protocol implementationcryptography

PDF

Garbage Collection for Rust: The Finalizer Frontier AKA: Alloy

OOPSLA 2025 language garbage collectiondestructor

PDF Code

GenC2Rust: Towards Generating Generic Rust Code from C AKA: GenC2Rust

ICSE 2025 c2rust genericstatic analysisvoid pointer

Code

Integrating Rules and Semantics for LLM-Based C-to-Rust Translation AKA: IRENE

ICSME 2025 c2rust LLMRAGstatic analysis

PDF

PALM: Synergizing Program Analysis and LLMs to Enhance Rust Unit Test Coverage AKA: PALM

ASE 2025 program analysis LLMharnessstatic analysisunit test

PDF

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees

OOPSLA 2025 formalization ownershipborrow checkertype checkerFloistryPrusti

PDF Code

Rug: Turbo LLM for Rust Unit Test Generation AKA: Rug

ICSE 2025 security fuzzing LLMharnessunit testMIRstatic analysis

PDF Code

RuMono: Fuzz Driver Synthesis for Rust Generic APIs AKA: RuMono

ACM TOSEM 2025 security fuzzing harnessgeneric

PDF Code

RustAssistant: Using LLMs to Fix Compilation Errors in Rust Code AKA: RustAssistant

ICSE 2025 program analysis LLMpatchcompilation error

PDF

RustAssure: Differential Symbolic Testing for LLM-Transpiled C-to-Rust Code AKA: RustAssure

ASE 2025 c2rust LLMdifferential testingsymbolic executionLLVM IR

PDF Code

RustRepoTrans: Repository-level Context Code Translation Benchmark Targeting Rust AKA: RustRepoTrans

ASE 2025 c2rust benchmarkLLM

PDF Code

RustyRTS: Regression Test Selection for Rust AKA: RustyRTS

ICST 2025 program analysis regression testregression test selection

Code

Safe4U: Identifying Unsound Safe Encapsulations of Unsafe Calls in Rust using LLMs AKA: Safe4U

ISSTA 2025 security LLMstatic analysissoundnessunsafeinvariantdocumentationencapsulation

PDF Code

Securing Mixed Rust with Hardware Capabilities AKA: CapsLock

CCS 2025 security FFIunsafeQEMU

PDF Code

Stack Filtering: Elevating Precision and Efficiency in Rust Pointer Analysis

CGO 2025 program analysis pointer analysislifetime

PDF Code

Thrust: A Prophecy-Based Refinement Type System for Rust AKA: Thrust

PLDI 2025 verification refinement type systemcorrectnessinvariantconstrained Horn clauseformalization

PDF Code

TickTock: Verified Isolation in a Production Embedded OS AKA: TickTock

SOSP 2025 verification Tockoperating systemisolation

PDF

Tock: From Research To Securing 10 Million Computers

SOSP 2025 product ecosystem

PDF Code

Towards Repository-Level Program Verification with Large Language Models AKA: RagVerus

LMPL 2025 verification proof generation LLMRAGVerus

PDF Code

Translating C To Rust: Lessons from a User Study

NDSS 2025 c2rust empirical studysafety

PDF

Tree Borrows

PLDI 2025 formalization soundnessundefined behavior

PDF

Trusting Code in the Wild: Exploring Contributor Reputation Measures to Review Dependencies in the Rust Ecosystem

IEEE TSE 2025 ecosystem empirical studycode reviewdependency

PDF

Type-Migrating C-to-Rust Translation Using a Large Language Model AKA: Tymcrat

Empirical Software Engineering 2025 c2rust LLMtype

PDF Code

TYPEPULSE: Detecting Type Confusion Bugs in Rust Programs AKA: TYPEPULSE

USENIX Security 2025 security type confusionstatic analysispointer analysisMIR

PDF Code

Unleashing the Efficiency of Rust: An Empirical Study of Performance Bugs in Rust Projects

ISSRE 2025 ecosystem empirical studyperformance

Code

VERT: Polyglot Verified Equivalent Rust Transpilation with Large Language Models AKA: VERT

ASE 2025 c2rust LLMmodel trainingfine tuneformalizationWeb Assemblymodel checker

PDF Code

Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust AKA: Vest

USENIX Security 2025 product verificationperformanceserializationparsing

PDF Code

Bigtools: a high-performance BigWig and BigBed library in Rust

Bioinformatics 2024 product bioinformatics

Code

SafeNet: Towards mitigating replaceable unsafe Rust code via a recommendation‐based approach AKA: SafeNet

STVR 2024 program analysis unsafemachine learningunsafe reduction

Code

Securing a Multiprocessor KVM Hypervisor with Rust AKA: KrustVM

SoCC 2024 product hypervisor

PDF

Taming shared mutable states of operating systems in Rust AKA: xv6Rust

SCP 2024 product operating system borrow checker

Code

Unishyper: A Rust-based unikernel enhancing reliability and efficiency of embedded systems AKA: Unishyper

JSA 2024 product operating system MPKunikernelembedded

Code

Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor AKA: HyperEncalve

ASPLOS 2024 verification TEEhypervisorMIR

PDF Code

A Context-Sensitive Pointer Analysis Framework for Rust and Its Application to Call Graph Construction AKA: Rupta

CC 2024 program analysis pointercall graphpointer analysis

PDF Code

A Study of Common Bug Fix Patterns in Rust AKA: Ruxanne

Empirical Software Engineering 2024 program analysis borrow checkerpatchempirical study

Code

An Empirical Study of Rust-for-Linux: The Success, Dissatisfaction, and Compromise

USENIX ATC 2024 ecosystem empirical studyRust for Linuxsecurityperformance

PDF Code

Automatically Enforcing Rust Trait Properties

VMCAI 2024 verification invarianttrait invariantKani

Code

Broadly Enabling KLEE to Effortlessly Find Unrecoverable Errors in Rust AKA: PanicCheck

ICSE-SEIP 2024 verification proof generation panicsymbolic execution

PDF

Cocoon: Static Information Flow Control in Rust AKA: Cocoon

OOPSLA 2024 program analysis information flow controlsecrecyintegrityeffect system

PDF Code

Crabtree: Rust API Test Synthesis Guided by Coverage and Type AKA: Crabtree

OOPSLA 2024 security fuzzing harnesstraitMiriafl.rsZ3

PDF

Demystifying Compiler Unstable Feature Usage and Impacts in the Rust Ecosystem

ICSE 2024 ecosystem unstable

PDF Code

Don't Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation AKA: Nopcrat

PLDI 2024 c2rust algebraic data typeoutput parameter

PDF Code

ERASan: Efficient Rust Address Sanitizer AKA: ERASan

IEEE S&P 2024 security sanitizer memory safety

PDF Code

Fearless Asynchronous Communications with Timed Multiparty Session Protocols AKA: MultiCrustyT

ECOOP 2024 product session type multiparty session typeasynchronoustimeout

PDF Code

Finding Performance Issues in Rust Projects

ASE 2024 ecosystem performanceempirical study

PDF Code

Formally Understanding Rust's Ownership and Borrowing System at the Memory Level AKA: RustSEM

Formal Methods in System Design 2024 formalization ownershipborrow checkermemory safety

FRIES: Fuzzing Rust Library Interactions via Efficient Ecosystem-Guided Target Generation AKA: FRIES

ISSTA 2024 security fuzzing harnessecosystemdependency

PDF

hax: Verifying Security-Critical Rust Software Using Multiple Provers AKA: hax

VSTTE 2024 verification cryptographycryptographic protocol implementation

Code

How Are Paid and Volunteer Open Source Developers Different? A Study of the Rust Project

ICSE 2024 ecosystem empirical studypayment

PDF

Is Unsafe an Achilles' Heel? A Comprehensive Study of Safety Requirements in Unsafe Rust Programming

ICSE 2024 security empirical studyunsafedocumentationinvariant

PDF Code

Leveraging Large Language Model to Assist Detecting Rust Code Comment Inconsistency AKA: RustC4

ASE 2024 program analysis documentation code-comment inconsistencyLLM

PDF

MetaSafe: Compiling for Protecting Smart Pointer Metadata to Ensure Safe Rust Integrity AKA: MetaSafe

USENIX Security 2024 security isolation smart pointermemory safetyMPKhardware

PDF Code

rCanary: Detecting Memory Leaks Across Semi-Automated Memory Management Boundary in Rust AKA: rCanary

IEEE TSE 2024 security model checkermemory leakSMTMIR

PDF Code

RefinedRust: A Type System for High-Assurance Verification of Rust Programs AKA: RefinedRust

PLDI 2024 verification proof generation refined typetype systemCoqMIR

PDF Code

RPG: Rust Library Fuzzing with Pool-Based Fuzz Target Generation and Generic Support AKA: RPG

ICSE 2024 security fuzzing harnessunsafe

PDF Code

Rust for Embedded Systems: Current State and Open Problems

CCS 2024 ecosystem embedded systemempirical studystatic analysis

PDF

Rust for Linux: Understanding the Security Impact of Rust in the Linux Kernel

ACSAC 2024 ecosystem Rust for Linuxsecurity

Code

Rust-lancet: Automated Ownership-Rule-Violation Fixing with Behavior Preservation AKA: Rust-lancet

ICSE 2024 program analysis patchownershipANFsymbolic executioncompilation error

PDF Code

Rust-twins: Automatic Rust Compiler Testing through Program Mutation and Dual Macros Generation AKA: Rust-twins

ASE 2024 security compiler LLMfuzzingdifferential testingharnessHIR

PDF Code

Rustlantis: Randomized Differential Testing of the Rust Compiler AKA: Rustlantis

OOPSLA 2024 security compiler fuzzingdifferential testingcorrectnessMIRLLVM

PDF Code

RustLIVE: Reducing the Learning Barriers of Rust Through Visualization AKA: RustLIVE

FIE 2024 language learningborrow checkerownership

RustSan: Retrofitting AddressSanitizer for Efficient Sanitization of Rust AKA: RustSan

USENIX Security 2024 security sanitizer HIRMIRunsafeLLVM

PDF Code

Semi-Automated Verification of Interior Unsafe Code Encapsulation in Real-World Rust Systems

ASE 2024 security encapsulationunsafe

PDF

Sound Borrow-Checking for Rust via Symbolic Semantics AKA: LLBC#

ICFP 2024 formalization borrow checker

PDF Code

SquirrelFS: Using the Rust Compiler to Check File-System Crash Consistency AKA: SquirrelFS

OSDI 2024 product type system

PDF Code

Surveying the Rust Verification Landscape

HATRA@SPLASH 2024 verification unsafesurvey

PDF

Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis AKA: Syzygy

arXiv 2024 c2rust LLMdynamic analysisI/Oprogram slicing

PDF Code

To Tag, or Not to Tag: Translating C's Unions to Rust's Tagged Unions AKA: Urcrat

ASE 2024 c2rust tagged unionpointer analysisMIR

PDF Code

Towards Translating Real-World Code with LLMs: A Study of Translating to Rust AKA: FLOURINE

arXiv 2024 c2rust LLMdifferential testingI/O

PDF

Understanding and Detecting Real-World Safety Issues in Rust AKA: lockbud

IEEE TSE 2024 ecosystem empirical studymemory safetyconcurrencypanicMIRdeadlock

PDF Code

Understanding Atomics and Memory Ordering Issues in Real-World Rust Software AKA: AtomVChecker

ISSRE 2024 security concurrency static analysisempirical studyatomicmemory ordering

Code

Unleashing the Power of Clippy in Real-World Rust Projects

ICSE Companion 2024 ecosystem empirical studydiagnoseclippy

PDF

UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking AKA: UnsafeCop

FM 2024 verification memory safetymodel checkerbounded model checkingunsafeMIR

PDF

Verus: A Practical Foundation for Systems Verification

SOSP 2024 verification

PDF Code

When Is Parallelism Fearless and Zero-Cost with Rust?

SPAA 2024 security concurrency empirical studyparallelism

PDF

Yuga: Automatically Detecting Lifetime Annotation Bugs in the Rust Language AKA: Yuga

IEEE TSE 2024 security lifetimepointer analysisHIRMIR

PDF Code

Rust-Shyper: A reliable embedded hypervisor supporting VM migration and hypervisor live-update AKA: Rust-Shyper

JSA 2023 product hypervisor

Code

"I wouldn't want my unsafe code to run my pacemaker": An Interview Study on the Use, Comprehension, and Perceived Risks of Unsafe Rust

USENIX Security 2023 ecosystem unsafesecurityempirical study

PDF

A Closer Look at the Security Risks in the Rust Ecosystem

ACM TOSEM 2023 security empirical studyecosystem

PDF Code

A Grounded Conceptual Model for Ownership Types in Rust AKA: Aquascope

OOPSLA 2023 language ownershipborrow checker

PDF Code

Adventure of a Lifetime: Extract Method Refactoring for Rust AKA: REM

OOPSLA 2023 language refactorextract methodlifetime

PDF Code

Aliasing Limits on Translating C to Safe Rust AKA: Laertes

OOPSLA 2023 c2rust empirical studypointeralias

PDF Code

An Empirical Study of Yanked Releases in the Rust Package Registry

IEEE TSE 2023 ecosystem empirical studydependencyyanked release

PDF

Assessing the Alignment between the Information Needs of Developers and the Documentation of Programming Languages: A Case Study on Rust

ACM TOSEM 2023 language documentation

PDF

Concrat: An Automatic C-to-Rust Lock API Translator for Concurrent Programs AKA: Concrat

ICSE 2023 c2rust concurrentlock

PDF Code

ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs AKA: ConDRust

ECOOP 2023 formalization concurrencycompiler

PDF Code

Flux: Liquid Types for Rust AKA: Flux

PLDI 2023 language liquid typeonwershipstack borrowrefined typeverification

PDF Code

Improving Automatic C-to-Rust Translation with Static Analysis

ICSE Companion 2023 c2rust static analysisunsafeconcurrencyoutput parameter

Leveraging Rust Types for Program Synthesis AKA: RusSOL

OOPSLA 2023 formalization program synthesistype systemownership

PDF Code

On the Dual Nature of Necessity in Use of Rust Unsafe Code

FSE 2023 language empirical studyunsafe

PDF Code

OOM-Guard: Towards Improving the Ergonomics of Rust OOM Handling via a Reservation-Based Approach AKA: OOM-Guard

FSE 2023 language memory managementstatic analysisLLVM IR

PDF Code

Ownership Guided C to Rust Translation AKA: CROWN

CAV 2023 c2rust ownershippointerSAT

PDF Code

Rust for Morello: Always-On Memory Safety, Even in Unsafe Code

ECOOP 2023 product memory safetyhardware

PDF Code

RustSmith: Random Differential Compiler Testing for Rust AKA: RustSmith

ISSTA 2023 security compiler differential testingfuzzinglifetimeborrow checker

PDF Code

SafeDrop: Detecting Memory Deallocation Bugs of Rust Programs via Static Data-Flow Analysis AKA: SafeDrop

ACM TOSEM 2023 security exception safetymemory safetydata-flow analysisstatic analysis

PDF Code

Specifying and Verifying Higher-Order Rust Iterators

TACAS 2023 verification Creusotiterator

PDF Code

SymRustC: A Hybrid Fuzzer for Rust AKA: SymRustC

ISSTA 2023 security fuzzing concolic executionLLVM IR

PDF Code

TRust: A Compilation Framework for In-process Isolation to Protect Safe Rust against Untrusted Code AKA: TRust

USENIX Security 2023 security isolation hardwareMPKFFILLVM IR

PDF Code

Verus: Verifying Rust Programs Using Linear Ghost Types AKA: Verus

OOPSLA 2023 verification linear ghost typeSMTlambda calculuspointerinterior mutabilityconcurrencyformalization

PDF Code

A tool-assisted approach to engineer domain-specific languages (DSLs) using Rust

MODELS 2022 product DSLEcoremetamodeling

PDF

Tighten rust’s belt: shrinking embedded Rust binaries

LCTES 2022 language embedded

PDF

Aeneas: Rust Verification by Functional Translation AKA: Aeneas

ICFP 2022 verification MIRLLBCunsafeCharon

PDF Code

Comprehensiveness, Automation and Lifecycle: A New Perspective for Rust Security

QRS 2022 ecosystem empirical studysecurity

PDF

Creusot: A Foundry for the Deductive Verification of Rust Programs AKA: Creusot

ICFEM 2022 verification ownershiptrait

Code

Cross-Language Attacks

NDSS 2022 security FFImemory safety

PDF Code

Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types AKA: Rumpsteak

PPoPP 2022 product session type asynchronousconcurrencydeadlocksession type

PDF Code

Detecting Cross-Language Memory Management Issues in Rust AKA: FFICHECKER

ESORICS 2022 security static analysis FFImemory management

Ferrite: A Judgmental Embedding of Session Types in Rust AKA: Ferrite

ECOOP 2022 product session type session type

PDF Code

Garbage Collection Makes Rust Easier to Use: A Randomized Controlled Trial of the Bronze Garbage Collector AKA: Bronze

ICSE 2022 language garbage collection

PDF Code

In rust we trust: a transpiler from unsafe C to safer rust AKA: CRustS2

ICSE Companion 2022 c2rust unsafe

PDF

Learning and Programming Challenges of Rust: A Mixed-Methods Study

ICSE 2022 ecosystem empirical studysafety

PDF Code

Memory-Safety Challenge Considered Solved? An In-Depth Study with All Rust CVEs

ACM TOSEM 2022 ecosystem empirical studymemory safetysecurity

PDF

Modular information flow through ownership AKA: Flowistry

PLDI 2022 program analysis information flowownershipOxide

PDF Code

On the Termination of Borrow Checking in Featherweight Rust

NFM 2022 formalization terminationborrow checker

PDF

PKRU-safe: automatically locking down the heap between safe and unsafe languages AKA: PKRU-safe

EuroSys 2022 security isolation PKRULLVM IRMPK

PDF Code

RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code AKA: RustHornBelt

PLDI 2022 verification unsoundfirst-order logic

PDF Code

RustViz: Interactively Visualizing Ownership and Borrowing AKA: RustViz

VL/HCC 2022 language learningownershipborrow checker

PDF Code

Search-Based Test Suite Generation for Rust AKA: RUSTYUNIT

SSBSE 2022 program analysis harnessunit test

Code

Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types AKA: MultiCrusty

ECOOP 2022 product session type panicmultiparty session type

PDF Code

The Prusti Project: Formal Verification for Rust

NFM 2022 verification Prusti

PDF Code

Towards Understanding the Runtime Performance of Rust

ASE 2022 language performancebenchmark

PDF Code

Verifying Dynamic Trait Objects in Rust

ICSE-SEIP 2022 verification traittrait objectMIR

PDF Code

A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust AKA: FeatherweightRust

ACM TOPLAS 2021 formalization compilerfuzzlifetimeborrow checker

PDF Code

Benefits and Drawbacks of Adopting a Secure Programming Language: Rust as a Case Study

SOUPS 2021 ecosystem survey

PDF

GhostCell: Separating Permissions from Data in Rust AKA: GhostCell

ICFP 2021 language interior mutabilitybranded type

PDF Code

Keeping Safe Rust Safe with Galeed AKA: Galeed

ACSAC 2021 security isolation MPKPKRULLVMhardware

PDF Code

MirChecker: Detecting Bugs in Rust Programs via Static Analysis AKA: MirChecker

CCS 2021 security static analysis MIRmemory safetySMTsymbolic execution

PDF Code

Modular Specification and Verification of Closures in Rust AKA: Prusti Closures

OOPSLA 2021 verification closureSMTfirst-order logic

PDF Code

Rudra: Finding Memory Safety Bugs in Rust at the Ecosystem Scale AKA: Rudra

SOSP 2021 security static analysis memory safetyunsafeexception safetytaint analysisdata-flow analysis

PDF Code

RULF: Rust Library Fuzzing via API Dependency Graph Traversal AKA: RULF

ASE 2021 security fuzzing harnessstatic analysis

PDF Code

Rupair: Towards Automatic Buffer Overflow Detection and Rectification for Rust AKA: Rupair

ACSAC 2021 security patch memory safetybuffer overflowdata-flow analysis

PDF

Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust AKA: NADER

OOPSLA 2021 security performanceunsafe

PDF Code

SyRust: Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis AKA: SyRust

PLDI 2021 program analysis harnessunit testownershipgeneric

PDF Code

Translating C to Safer Rust

OOPSLA 2021 c2rust safetyempirical study

PDF Code

Firecracker: Lightweight Virtualization for Serverless Applications AKA: Firecracker

NSDI 2020 product operating system virtual machine monitor

PDF Code

How Do Programmers Use Unsafe Rust? AKA: Qrates

OOPSLA 2020 ecosystem unsafeempirical study

PDF Code

Implementing Multiparty Session Types in Rust AKA: mpst-rust

COORDINATION 2020 product session type multiparty session typesession type

PDF Code

Is Rust Used Safely by Software Developers?

ICSE 2020 ecosystem unsafe

PDF

RedLeaf: Isolation and Communication in a Safe Operating System AKA: RedLeaf

OSDI 2020 product operating system isolation

PDF Code

RustBelt Meets Relaxed Memory

POPL 2020 verification concurrency

PDF Code

RusTEE: Developing Memory-Safe ARM TrustZone Applications AKA: RusTEE

ACSAC 2020 product TEEARM TrustZonehardware

PDF Code

RustHorn: CHC-Based Verification for Rust Programs AKA: RustHorn

ESOP 2020 verification constrained Horn clausepointerownership

PDF Code

Securing Unsafe Rust Programs with XRust AKA: XRust

ICSE 2020 security isolation unsafedata-flow integrity

PDF Code

Stacked Borrows: An Aliasing Model for Rust

POPL 2020 formalization soundnessundefined behavior

PDF

Theseus: An Experiment in Operating System Structure and State Management AKA: Theseus

OSDI 2020 product operating system

PDF Code

Towards making formal methods normal: meeting developers where they are AKA: RVT

HATRA@SPLASH 2020 verification symbolic execution

PDF

Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs

PLDI 2020 ecosystem memory safetyconcurrencyempirical studyunsafe

PDF Code

VRLifeTime - An IDE Tool to Avoid Concurrency and Memory Bugs in Rust AKA: VRLifeTime

CCS 2020 language learninglifetimeconcurrency

PDF Code

Fearless Concurrency? Understanding Concurrent Programming Safety in Real-World Rust Software

arXiv 2019 security concurrency empirical studydeadlockdata race

PDF

Leveraging Rust Types for Modular Specification and Verification AKA: Prusti

OOPSLA 2019 verification correctnessmemory safetyMIR

PDF Code

Oxide: The Essence of Rust AKA: Oxide

arXiv 2019 formalization type systemtype checker

PDF Code

Rusty Variation: Deadlock-free Sessions with Failure in Rust AKA: Rusty Variation

ICE (EPTCS) 2019 product session type deadlock

PDF Code

Towards Memory Safe Enclave Programming with Rust-SGX AKA: Rust-SGX

CCS 2019 product Intel SGXhardwareformalizationFFIsecurity

PDF Code

KRust: A Formal Executable Semantics of Rust AKA: KRust

TASE 2018 formalization verification

PDF

No Panic! Verification of Rust Programs by Symbolic Execution AKA: cargo-klee

INDIN 2018 verification panickleesymbolic executionLLVM IR

Code

RustBelt: Securing the Foundations of the Rust Programming Language AKA: RustBelt

POPL 2018 formalization safetylambda calculusunsafeIrisCoq

PDF Code

Verifying Rust Programs with SMACK AKA: SMACK

ATVA 2018 verification LLVM IR

PDF Code

Multiprogramming a 64kB Computer Safely and Efficiently AKA: Tock

SOSP 2017 product operating system hardware

PDF Code

Sandcrust: Automatic sandboxing of unsafe components in rust AKA: Sandcrust

PLOS@SOSP 2017 security isolation unsafeFFI

PDF Code

System Programming in Rust: Beyond Safety

HotOS 2017 language linear typeinformation flow analysisfault isolation

PDF

Rust-Bio: a fast and safe bioinformatics library AKA: Rust-Bio

Bioinformatics 2016 product bioinformatics

PDF Code

Engineering the Servo Web Browser Engine Using Rust

ICSE Companion 2016 product

PDF Code

Rust as a Language for High Performance GC Implementation

ISMM 2016 product garbage collection

PDF Code

Crust: A Bounded Verifier for Rust AKA: Crust

ASE 2015 verification memory safetypointer aliasharness

Fuzzing the Rust Typechecker Using CLP (T)

ASE 2015 security compiler type checkerfuzzingCLP

PDF

Patina: A Formalization of the Rust Programming Language AKA: Patina

2015 formalization borrow checkermemory safety

PDF

Session Types for Rust

WGP@ICFP 2015 product session type

PDF Code

The Rust Language

HILT (ACM SIGAda) 2014 language

PDF Code

Awesome Rust Papers Explorer

Analytics

Papers by Year

Papers by Category

Papers by Venue

Papers by Tag