Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications

Fanpeng Yang, Xu Ma, Shuling Wang +5

Automatically generating formal specifications including loop invariants, preconditions, and postconditions for legacy code is critical for program understanding, reuse and verific…