  Relational properties describe relationships that hold over multiple
executions of one or more programs, such as functional equivalence.
Conventional approaches for automatically verifying such properties typically
rely on syntax-based, heuristic strategies for finding synchronization points
among the input programs. These synchronization points are then annotated with
appropriate relational invariants to complete the proof. However, when
suboptimal synchronization points are chosen the required invariants can be
complicated or even inexpressible in the target theory.
  In this work, we propose a novel approach to verifying relational properties.
This approach searches for synchronization points and synthesizes relational
invariants simultaneously. Specifically, the approach uses synthesized
invariants as a guide for finding proper synchronization points that lead to a
complete proof. We implemented our approach as a tool named PEQUOD, which
targets Java Virtual Machine (JVM) bytecode. We evaluated PEQUOD by using it to
solve verification challenges drawn from the from the research literature and
by verifying properties of student-submitted solutions to online challenge
problems. The results show that PEQUOD solve verification problems that cannot
be addressed by current techniques.
