Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic

Explore a conference presentation that introduces a novel encoding theory for reducing ∀∃ relational Hoare logic to standard unary Hoare logic. Learn how researchers from Shanghai Jiao Tong University address the complexity challenges in program verification by proposing a generic approach that preserves original proof rules while encapsulating the ∀∃ pattern within assertions. Discover how this method enables verification of real-world program functional correctness through refinement proofs and algorithm correctness proofs without requiring modifications to existing logic frameworks. Understand the theoretical foundations that demonstrate how relational Hoare logic proof rules are special cases of standard Hoare logic rules, and how relational proof steps correspond to standard proof steps. Examine the practical implications of this encoding theory for program refinement verification in nondeterministic settings, including the introduction of the Exec predicate that allows standard Hoare logic to prove ∀∃ relational properties. Gain insights into how this approach reduces formalization complexity and soundness proof overhead compared to existing methods that rely on ghost states and invariants, making formal verification more accessible and efficient for practitioners working with complex program verification tasks.