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

Last commit date

26 January 2021

Related papers

https://doi.org/10.1007/978-3-030-53291-8_9

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.