Program
Verification
Book

PV2 ⊧ Path Analysis for invariant Generation by Abstract Interpretation (PAGAI)computes inductive invariants on the numerical variables of a given program

Type of tool

Invariant generator

Links

http://web.archive.org/web/20171130171403/http://pagai.forge.imag.fr/ (original page inaccessible)

Related papers

PAGAI: A Path Sensitive Static Analyser (TAPAS 2012)
Succinct Representations for Abstract Interpretation (SAS 2012)

ProVerB specific

Markdown description: view/edit
Contained in the ProVerB22 dataset (paper + artefact)

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