Automated Discovery of Loop Invariants for High-Assurance Programs Synthesized Using AI Planning Techniques

The discovery of loop invariants is a great challenge for the independent verification of automatically synthesized programs. This verification is needed to achieve high confidence in the correctness of the synthesized code, i.e., assurance that no latent defects in the synthesizer itself could have led to the synthesis of an incorrect program. To address this problem, we present an automated loop invariant discovery approach for programs synthesized using a combination of AI planning and component-based software development techniques. Specifically, a plan (denoting the synthesized code) is generated by an enhanced Graphplan planner first. The loop invariants can be automatically discovered based on the same planning graph used to synthesize the code. The correctness can be independently verified via standard loop invariant proof steps, including initialization, maintenance, and termination. The proposed approach not only has a rigorous theoretical basis, but is also guaranteed to produce accurate invariants by removing spurious invariants that are independent of the concerned loop. In combination with other loop invariant detection techniques, the proposed approach can produce loop invariants for complex programs and, thus, greatly facilitate high-confidence automated verification of synthesized systems.