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

Application domain/field

Type of tool

Invariant generator

Expected input

Format:

Expected output

Invariant inv such that T can be verified with check

Internals

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.
C CHC

Links

Repository: https://github.com/PL-ML/code2inv

Related papers

Code2Inv: A Deep Learning Framework for Program Verification

Last publication date

14 July 2020

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.