Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning

Minchao Wu, Takeshi Tsukada, Hiroshi Unno +2

Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Desp…