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.
Jicheng Fu Farokh B.Bastani I-Ling Yen
Department of Computer Science University of Texas at Dallas
国际会议
11th IEEE High Assurance Systems Engineering Symposium(HASE 2008)(第十一届IEEE高可信系统工程国际研讨会)
南京
英文
333-342
2008-12-03（万方平台首次上网日期，不代表论文的发表时间）