PV2 ⊧ LoopInvGentransforms program's assertions into an equivalent loop invariant

Tool to generate sufficient loop invariants for program verification

Application domain/field

• Invariant inference
• Program verification
• Data-driven inference
• Syntax-guided synthesis (SyGuS)

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