PV5 Attestorchecks if a property holds for a program, generates additional properties, provides examples and analysis logs

Application domain/field

Type of tool

Model checker

Expected input


Expected output

  1. Computed abstract state space
  2. Derived procedure contracts
  3. Model checking results, for each LTL formula either: formula satisfied, formula (definitely) not satisfied or formula possibly not satisfied. In case it is (possibly) not satisfied, a counterexample is produced (an abstract trace that violates the LTL formula, possibly a concrete initial heap).
  4. General information about the analysis: log messages, details about settings and runtime of analyses


Symbolic execution is used to construct an abstract state space


The Github repository has an extensive wiki which describes things such as the graph grammar syntax. It is possible to use a settings file (.attestor) that is a collection of command-line options which can then be imported with the tool.
Java LTL Model checking


Related papers

Let this Graph Be Your Witness!

Last publication date

18 July 2018

Related tools

Forester, Groove, Infer, HIP/SLEEK, Korat, Juggernaut, Tvla

ProVerB specific

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