Forall-Exists Relational Verification by Filtering to Forall-Forall

Ramana Nagasamudram, Anindya Banerjee, David A. Naumann

Relational verification encompasses research directions such as reasoning about data abstraction, reasoning about security and privacy, secure compilation, and functional specifica…