9 papers
Codoku: Renewable Program-Reasoning Challenges for Frontier Coding Agents
Cong Li, Hao Sun, Zenan Li +1
Existing program-reasoning benchmarks ask large language models to predict a program's behavior on a given input. Coding agents break two assumptions on which these benchmarks rest…
Learning to Disprove: Formal Counterexample Generation with Large Language Models
Zenan Li, Zhaoyu Li, Kaiyu Yang +2
Mathematical reasoning demands two critical, complementary skills: constructing rigorous proofs for true statements and discovering counterexamples that disprove false ones. Howeve…
Agentic Harness for Real-World Compilers
Yingwei Zheng, Cong Li, Shaohua Li +2
Compilers are critical to modern computing, yet fixing compiler bugs is difficult. While recent large language model (LLM) advancements enable automated bug repair, compiler bugs p…
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Baoding He, Zenan Li, Wei Sun +4
Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual a…
Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
Zenan Li, Ziran Yang, Deyuan He +7
Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness. Formally verifying that implementations satisfy specifications requires constr…
Cross-Ecosystem Vulnerability Analysis for Python Applications
Georgios Alexopoulos, Nikolaos Alexopoulos, Thodoris Sotiropoulos +3
Python packages often bundle third-party native libraries (e.g., OpenSSL), a practice known as vendoring. Identifying vulnerabilities in these libraries is challenging because curr…
An Empirical Study of Rust-Specific Bugs in the rustc Compiler
Zixi Liu, Yang Feng, Yunbo Ni +5
Rust is gaining popularity for its well-known memory safety guarantees and high performance, distinguishing it from C/C++ and JVM-based languages. Its compiler, rustc, enforces the…
SAND: Decoupling Sanitization from Fuzzing for Low Overhead
Ziqiao Kong, Shaohua Li, Heqing Huang +1
Sanitizers provide robust test oracles for various software vulnerabilities. Fuzzing on sanitizer-enabled programs has been the best practice to find software bugs. Since sanitizer…
UBfuzz: Finding Bugs in Sanitizer Implementations
Shaohua Li, Zhendong Su
In this paper, we propose a testing framework for validating sanitizer implementations in compilers. Our core components are (1) a program generator specifically designed for produ…