PV2 LoopInvGentransforms program's assertions into an equivalent loop invariant

Tool to generate sufficient loop invariants for program verification

Application domain/field

Type of tool

Synthesis tool/Loop invariant generator

Expected input

SyGuS problem


.sl file (SyGuS format)

Expected output

A loop invariant such that we can prove that program's assertions will never fail. (I'm unsure about the format in which it presents the results)


Uses Escher, Z3


Repository: https://github.com/SaswatPadhi/LoopInvGen

Related papers

Last publication date

12 July 2019

ProVerB specific

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