PPubMed16 Jun 2020Cited 37×

Code2Inv: A Deep Learning Framework for Program Verification

Shuvendu K. Lahiri, Chao Wang, Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, Le Song

Abstract

'Mayur Naik' 'Le Song'] We propose a general end-to-end deep learning framework Code2Inv, which takes a verification task and a proof checker as input, and automatically learns a valid proof for the verification task by interacting with the given checker. Code2Inv is parameterized with an embedding module and a grammar: the former encodes the verification task into numeric vectors while the latter describes the format of solutions Code2Inv should produce. We demonstrate the flexibility of Code2Inv by means of two small-scale yet expressive instances: a loop invariant synthesizer for C programs, and a Constrained Horn Clause (CHC) solver.

A figure from Code2Inv: A Deep Learning Framework for Program Verification — fig. from the paper

§ The Valyu brief

The paper, in five minutes

Read from the full text via Valyu Contents

Code2Inv uses deep learning and reinforcement learning to automatically synthesize program invariants, outperforming existing solvers and showing transferability and flexibility.

What’s new

i.Introduces Code2Inv, a framework that combines graph neural networks, Tree‑LSTM, attention, and policy‑gradient reinforcement learning for program verification.
ii.Demonstrates two instances: a loop‑invariant synthesizer for C programs and a Constrained Horn Clause (CHC) solver.
iii.Evaluates Code2Inv on 133 C programs, showing superior verification cost and transferability compared to three state‑of‑the‑art tools.
iv.Performs case studies on flexibility (different invariant classes) and naturalness of generated invariants.

How they did it

Code2Inv encodes verification tasks as graph representations using GNNs and defines a grammar for invariant structures. A neural policy, trained via deep reinforcement learning, iteratively generates invariants by sampling actions guided by attention over embeddings and receives continuous rewards based on counterexample satisfaction. The learned policy can be transferred to similar programs or adapted to new domains by swapping the checker or grammar.

What they found

Solved 133 C benchmark programs, outperforming C2I, LoopInvGen, and ICE‑DT in verification cost (number of Z3 queries).
Solved 94 of 120 CHC instances (Spacer solved 112, LinearArbitrary 118).
Solved 5 of 7 non‑linear CHC instances, whereas Spacer and LinearArbitrary solved none.
90% of solved C instances finished within 2 h; the remaining required up to 12 h.

Caveats

✕Does not support programs with multiple loops, function calls, or recursion.
✕Generally slower than some contemporary approaches (up to 12 h for hardest cases).
✕Performance depends on CPU; could improve with GPUs or more efficient training.

§ The Valyu brief

Reading the full paper and taking notes. This takes a few seconds…

§ Ask this paper

Ask a question about this paper

Valyu reads the full text and answers from what the paper actually says.

§ Related work in other archives

Code2Inv: A Deep Learning Framework for Program Verification

The paper, in five minutes

Ask a question about this paper

Similar papers in all four archives

The paper, in five minutes

Similar papers in all four archives