基于UnsatCore和强化学习的循环不变式模板生成方法

本发明公开了一种基于Unsat Core和强化学习的循环不变式模板生成方法，包括：步骤S1：建立基于自主强化学习的循环不变式模板生成器；通过强化学习，在Unsat Core的信息指导下学习到如何生成“有效循环不变式模板”；步骤S2：建立基于SMT求解器的循环不变式模板求解器；用来求解模板系数，从而生成有效循环不变式候选；当求解失败时，则用来提供模板的Unsat Core不可满足核；步骤S3：建立Unsat Core的模板归因分析器；用来对SMT提供的不可满足核进行分析，并归因到不变式模板的具体生成过程中，指导强化学习模型进行归因学习和迭代的模板完善过程。本发明具有原理简单、稳定性高且操作便捷高效等优点。