Compositional Loop Invariant Inference for Multiphase Programs via Structured Neurosymbolic Reasoning

Mingxiu Wang, Jiawei Wang, Shuangxiang Kan +4

Loop invariants are essential for deductive program verification, yet automatically inferring them for {multiphase programs}, whose loops contain conditional branches that induce m…