Features of Code2Inv

---

Transferability

Code2Inv learns a neural policy for each benchmark while learning its invariant. The neural policy learned depends on the graph structure of the program including components like variables, constants, control flow, data flow and others. As such, this learned neural policy can be used to accelerate the search for invariants in other similar programs.

Flexibility

Code2Inv is built to be flexible. We demonstrate the ability of Code2Inv to learn invariants for C programs as well as act as a CHC solver, both using the same general framework but with different front-ends. We also demonstrate the ability of Code2Inv to solve non-linear CHC tasks by simply changing the grammar of the expected invariant. We describe the general process involved in customizing Code2Inv in the customizing.md file in our GitHub repository.

Naturalness

Solutions discovered by Code2Inv tend to be more natural and more easily understandable, which allows people to more easily use Code2Inv. The naturalness does depend on the grammar of the invariant.