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…