# PV2 ⊧ Code2Invgenerates invariants from a C or CHC program, requires an external solver

### Application domain/field

- Loop invariant generation
- Constrained Horn Clause (CHC) solving

### Type of tool

Invariant generator### Expected input

- Verification instance
- Proof checker
*check*

Format:

*Verification instance*: C program (only supports one loop and no external funciton calls) or a CHC program*Proof checker*: ? (a function that takes a verification instance T and a candidate invariant inv, it then either returns success or a counterexample. For example an SMT or CHC solver)

### Expected output

Invariant*inv*such that T can be verified with

*check*

### Internals

- Deep learning
- Reinforcement learning