The \pate{} verifier is a static relational verification tool designed to ensure that security micropatches applied to binaries are safe and free from unintended consequences.
The verifier generates detailed reports that precisely identify the conditions under which two binary versions exhibit identical behavior.
This equivalence information can reveal any unforeseen side effects of a binary patch, such as changes to program behaviors beyond those intended by the original fix.

The verifier is intended to enable users to:
\begin{itemize}
\item precisely reason about the effects of patches applied to binaries,
\item explain potential differences in observable behaviors, accounting for all possible execution paths, and thus
\item reduce the time required to develop safe binary patches.
\end{itemize}
