Alcino Cunha, Hugo Pacheco, Nuno Macedo: HyperLasso: Bounded Model Checking of ∀<sup>+</sup>∃><sup>+</sup>-Liveness Hyperproperties. CAV (1) 2026: 473-496