Reviews: Learning Loop Invariants for Program Verification

The paper presents a novel deep network architecture termed DELPHI to automatically infer loop invariants for use in program verification. The architecture takes in as input source code which has (1) a number of assumption or assignment statements, (2) a loop with nested if-else statements with arithmetic operations and (3) a final assertion statement. The output of the architecture is a loop invariant in CNF which holds true at every iteration in the loop, and for which the assertion (3) is true after the loop ends execution. The architecture represents the source code AST using a graph-structured neural network, and treats it as a structured memory which it repeatedly accesses through attention operations. The generation of the CNF invariant is broken up into a sequential decision-making process where at each time the architecture predicts an output (op, T), where op is either && or and T is a simple logical expression.