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

Format:

.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)

Internals

Uses Escher, Z3
SyGuS

Links

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

Last commit date

23 April 2020

Related papers

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



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