PV4 EAHyperchecks satisfiability, implication and equivalence of hyperproperties

Tool for the automatic checking of satisfiability, implication and equivalence of hyperproperties.

Application domain/field

Type of tool

Satisfiability solver

Expected input

HyperLTL formula in the ** fragment, or an implication between two alternation-free formulas.

Expected output



License: ISC License


Related papers

EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties (CAV '17)

Last publication date

13 July 2017

Related tools

Possibly related: MCHyper

ProVerB specific

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