5 papers
How Powerful are LLMs in Generating Formal Program Specifications?
Fanpeng Yang, Xing Li, Shuling Wang +7
Formal verification provides strong guarantees of software correctness, but its adoption is limited by the high cost of writing precise formal specifications. While recent large la…
KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base
Wenhan Wang, Zeyu Sun
Automated formal specification generation is a key step towards program understanding and formal verification. Recently, due to the success of large language models (LLMs) in code…
SpecRL: Reinforcement Learning with Test-Based Completeness Rewards for Formal Specification Synthesis
Zhechong Huang, Zhao Zhang, Zeyu Sun +2
Specification synthesis asks a model to generate specifications and auxiliary annotations for an existing program. In modern software verification projects, specification accuracy…
Can Large Language Models Reason About Complex Execution Paths? An Empirical Study on Python
Wenhan Wang, Kaibo Liu, Zeyu Sun +4
Execution path reasoning is a key step towards program semantics understanding. It is crucial for generating test cases that cover certain branches/paths, or detecting bugs that ar…
Interleaved Learning and Exploration: A Self-Adaptive Fuzz Testing Framework for MLIR
Zeyu Sun, Jingjing Liang, Weiyi Wang +3
MLIR (Multi-Level Intermediate Representation) has rapidly become a foundational technology for modern compiler frameworks, enabling extensibility across diverse domains. However,…