HyperLasso: Bounded Model Checking of ∀+∃>+-Liveness Hyperproperties

Abstract This paper presents the first symbolic bounded model checking technique capable of verifying $\forall ^+\exists ^+$ ∀ + ∃ + -liveness hyperproperties (expressed in HyperLTL) over arbitrary (non-terminating) reactive systems. Previous bounded procedures for HyperLTL handled only safety hyperproperties or arbitrary properties over terminating systems. We implement our technique as HyperLasso . Our evaluation results show that it consistently outperforms the explicit-state complete model checker AutoHyper (the only existing tool capable of automatically verifying this class of problems) at several complex bug-finding and synthesis problems.