KestRel: Relational Verification Using E-Graphs for Program Alignment

Robert Dickerson, Prasita Mukherjee, Benjamin Delaware

Many interesting program properties involve the execution of multiple programs, including observational equivalence, noninterference, co-termination, monotonicity, and idempotency.…