Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts. This requirement has become a major bottleneck as large language models (LLMs) increasingly generate low-level systems code whose correctness cannot be assumed. To enable scalable formal verification, we focus exclusively on function specification generation, deliberately avoiding the synthesis of complex loop invariants that are central to traditional verification pipelines. We propose a neuro-symbolic framework for automatically generating memory-aware formal function specifications for C programs from natural language problem descripti...
| Authors | Liao Zhang, Tong Chen, Xiwei Wu et al. |
|---|---|
| Primary category | cs.SE |
| Published | 12 March 2026 |
| Last updated at source | 12 March 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.