Hyper Hoare Logic: A Unified Approach to Proving and Disproving Program Hyperproperties

Hyper Hoare Logic is a novel program logic that can prove or disprove arbitrary hyperproperties over terminating program executions, including properties that no existing Hoare logic can express.