Forall-Exists Relational Verification by Filtering to Forall-Forall

Ramana Nagasamudram, Anindya Banerjee, David A. Naumann +1

Relational verification encompasses reasoning about data abstraction, security and privacy, secure compilation, and functional specification of tensor programs, among others. Sever…