RHLE: Modular Deductive Verification of Relational $\forall \exists$ Properties

Robert Dickerson, Qianchuan Ye, Michael K. Zhang +1

Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about…