Sep, 2023

动态和控制模型的通用验证框架与证书合成

TL;DR我们提供了一个对系统规范进行编码和定义相关证明的通用框架,并提出了一种自动化的方法来形式合成控制器和证明,通过利用神经网络的灵活性提供候选控制和证明函数,同时使用 SMT 求解器提供正确性的正式保证,我们通过开发一个原型软件工具对我们的框架进行测试,并评估其在通过对广泛的基准测试进行控制和证明合成时的有效性。