程序分析与验证是计算机科学中的重要研究课题之一。近年来,随着深度学习技术的发展,深度学习方法已被广泛应用于程序分析与验证。本文基于深度学习和反例制导研究了数值程序的Craig插值生成和秩函数生成等问题,主要研究内容如下:·Craig插值技术是循环程序不变式生成的有效方法。针对非线性组合理论下的Craig插值生成问题,本文提出了基于深度学习和形式验证的神经网络型Craig插值的生成方法。该方法首先运用监督学习算法有效构造候选的Craig插值,再结合可满足性模理论（Satisfiability Modulo Theories,SMT）求解技术严格保证Craig插值的正确性。进一步,基于Craig插值生成方法实现了循环不变式的自动生成。·秩函数生成技术是循环程序终止性判定的有效方法。针对非线性循环程序,本文提出了一种基于深度学习和反例制导的神经网络型秩函数的构造方法。该方法采用学习组件和验证组件交互的迭代框架,其中学习组件利用程序轨迹作为训练集构造候选秩函数,验证组件运用SMT求解技术严格保证候选秩函数的有效性,由SMT求解器返回的反例则进一步应用于候选秩函数的迭代精化。该方法较已有的机器学习方法在秩函数的构造效率和构造能力上具有优势。·实现了数值程序的Craig插值生成工具Synthe NI和秩函数生成工具Synthe RF,能有效生成神经网络型Craig插值和秩函数。