Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)

Jianan Yao, Gabriel Ryan, Justin Wong +2

Verifying real-world programs often requires inferring loop invariants with nonlinear constraints. This is especially true in programs that perform many numerical operations, such…