代码大模型 / AI 编程

Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning

神经形式化验证：智能体的语言无关形式化程序推理

Shuvendu K. Lahiri

专题命中 程序分析与验证 ：coding agent(abstract)；分类 cs.SE、cs.PL

AI总结 该研究提出神经形式化验证（NFV），让AI编码智能体与成熟验证器结合，为主流语言开发者实现一键式程序验证，在Python编程问题数据集上取得了良好的验证效果。

VeGo: Direct Deductive Formal Verification of Go Programs for Computer Science Education

VeGo：面向计算机科学教育的Go程序直接演绎形式化验证

Tina Massoudi, Chris Dutchyn

专题命中 程序分析与验证 ：coding agent(abstract)；分类 cs.PL

AI总结 该研究提出面向计算机科学教育的VeGo系统，可直接验证标准Go程序，整合多种形式化验证技术，对比其他语言论证Go的优势，经教育教材评估并规划了形式并发规约的路线图。

Comments 13 pages + 2 pages of references, 5 code displays, ancillary reference manual for VeGo