PV3 HyPA (Hyperproperty Verification with Predicate Abstraction)checks $\forall^k \exists^l$-safety properties of a model

Application domain/field

Expected input


.hypa file listing the following:


Used to verify kl-safety properties within a given abstraction. This means that for any k traces, there exist l traces such that the resulting k+l traces do not interact badly. It can also be used for k-safety verification, i.e. no bad interaction occurs between any k traces. A k-safety property is equivalent to a kl-safety property where l=0. It uses the temporal logic Observation-based HyperLTL (OHyperLTL), an extension of HyperLTL. Uses Z3 to discharge SMT queries.
HyperLTL Hyperproperties Infinite-state systems Predicate abstraction


Related papers

Software Verification of Hyperproperties Beyond k-Safety (CAV 2022)

Last publication date

7 August 2022

ProVerB specific

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