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

Internals

Comments

License: ISC License
HyperLTL

Links

Last commit date

18 July 2018

Related papers

https://doi.org/10.1007/978-3-319-63390-9_29 (CAV '17)

Last publication date

13 July 2017

Related tools

Possibly related: MCHyper

ProVerB specific

View/edit source (Markdown)



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