  We present SilVer (Silq Verification), an automated tool for verifying
behaviors of quantum programs written in Silq, which is a high-level
programming language for quantum computing. The goal of the verification is to
ensure correctness of the Silq quantum program against user-defined
specifications using SMT solvers. We introduce a programming model that is
based on a quantum RAM-style computer as an interface between Silq programs and
SMT proof obligations, allowing for control of quantum operations using both
classical and quantum conditions. Additionally, users can employ measurement
flags within the specification to easily specify conditions that measurement
results require to satisfy for being a valid behavior. We provide case studies
on the verification of generating entangled states and multiple oracle-based
algorithms.
