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

Application domain/field

• Hyperproperties
• Temporal hyperproperties
• Infinite-state systems
• Predicate abstraction

Expected input

• Symbolic Transition System (STS)
• OHyperLTL property
• predicates to be used for the abstraction

Format:

.hypa file listing the following:

• list of files for the symbolic transition systems
• file that contains the safety automaton
• quantifier structure of the hyperproperty
• file containing the predicates that should be used

• STS: file listing variables, locations, transitions, and where the program is observed. More details on this format can be found in the repo.
• Property: Specified as a safety automaton, similar to how the STS is specified. More details about the format can be found in the repo.
• Predicates: More details about the format can be found in the repo.

Internals

Used to verify ${\forall }^k{\exists }^l$-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 ${\forall }^k{\exists }^l$-safety property where $l=0$. It uses the temporal logic Observation-based HyperLTL (OHyperLTL), an extension of HyperLTL. Uses Z3 to discharge SMT queries.