BriefGPT.xyz
Sep, 2019
使用连续逻辑网络学习循环不变量
CLN2INV: Learning Loop Invariants with Continuous Logic Networks
HTML
PDF
Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gui, Suman Jana
TL;DR
本文提出了一种新的神经网络体系结构 Continuous Logic Network (CLN),可以从程序执行路径中直接自动学习循环不变量,使用新的SMT公式嵌入方法,实现了完整且精确的自动化推理,并展示了其在各自领域中的性能优势。
Abstract
program verification
offers a framework for ensuring program correctness and therefore systematically eliminating different classes of bugs. Inferring
loop invariants
is one of the main challenges behind automate
→