代码大模型 / AI 编程

Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm

线性模型预测控制的验证实验：内点法算法的自动生成与形式验证

Guillaume Davy, Eric Féron, Pierre-Loïc Garoche, Didier Henrion

专题命中 程序分析与验证 ：code generation(abstract)

AI总结 本文研究了线性模型预测控制中内点法算法的自动生成与形式验证，通过代码专门化阶段生成额外的注释来形式化算法的意图规范，并利用演绎方法自动证明这些断言的有效性，同时通过SMT求解器验证整个证明过程。

Journal ref 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-22), Nov 2018, Awassa, Ethiopia. https://easychair.org/smart-program/LPAR-22/