Bin Yu

NL2VBench: A Benchmark for End-to-End Natural-Language to Verifiable Rust Generation

Large language models (LLMs) have shown promise in code generation, but generating formally verifiable Rust programs from natural-language descriptions remains highly challenging. We present a benchmark called NL2VBench for generating verifiable Rust programs from natural-language descriptions using Verus.NL2VBench con...

Understanding the Performance-Effectiveness Trade-Offs of AddressSanitizer in Real-World Programs: An Empirical Study

AddressSanitizer (ASan) is widely deployed in industrial C/C++ development, but its runtime and memory costs can limit routine use in continuous integration and production-like testing. Although many optimized ASan-like sanitizers have been proposed, heterogeneous workloads, configurations, and baselines make their pra...

DafnyRAG: A Retrieval-Augmented and Verification-Driven Tool for Automated Repair of Dafny Code

Verifying Interrupt-driven Programs Efficiently via Heuristic and Reduced Partial-order Constraints

A model checking approach for detecting assertion violations in interrupt-driven programs by considering the unique enable-before mechanism specific to interrupt-driven programs, infeasible partial-order constraints are identified and eliminated, resulting in a simplified formula for more efficient reasoning.

IDPVerifier: Verifying Interrupt-driven Programs Efficiently via Heuristic and Reduced Partial-order Constraints

A model checking approach that leverages interrupt mechanisms to prune the search space at the constraint-encoding stage, showing how leveraging interrupt semantics in constraint encoding can mitigate the state-space explosion in verifying complex embedded software.