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

Comments

Framework for program verification based on deep learning. Given a verification task and proof checker as input, it automatically learns a valid proof for the verification task by interacting with the given checker.