5 papers
Constrained Code Generation with Discrete Diffusion
Lize Shao, Michael Cardei, Zichen Xie +2
Discrete diffusion models are a powerful, emerging paradigm for code generation. They construct programs through iterative refinement of partially corrupted token sequences and ena…
VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
Zichen Xie, Mrigank Pawagi, Yuxin Liu +5
Large language models can generate useful code from natural language, but their outputs come without correctness guarantees. Verifiable code generation offers a path beyond testing…
Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought
Zichen Xie, Wenxi Wang
As Large Language Models (LLMs) increasingly assist secure software development, their ability to meet the rigorous demands of Rust program verification remains unclear. Existing e…
Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API Misuse Detection in the Era of LLMs
Yifan Xia, Zichen Xie, Peiyu Liu +4
While the automated detection of cryptographic API misuses has progressed significantly, its precision diminishes for intricate targets due to the reliance on manually defined patt…
KNighter: Transforming Static Analysis with LLM-Synthesized Checkers
Chenyuan Yang, Zijie Zhao, Zichen Xie +2
Static analysis is a powerful technique for bug detection in critical systems like operating system kernels. However, designing and implementing static analyzers is challenging, ti…