CLN2INV: Learning Loop Invariants with Continuous Logic Networks

Understand

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 automated verification of real-world programs which often contain many loops.
• In this paper, we present Continuous Logic Network (CLN), a novel neural architecture for automatically learning loop invariants directly from program execution traces.
• Unlike existing neural networks, CLNs can learn precise and explicit representations of formulas in Satisfiability Modulo Theories (SMT) for loop invariants from program execution traces.