Verifying programs for quantum computers

Over the last three decades, quantum computing as a field has drawn much more attention. In recent years, first computers taking advantage of the effects of quantum mechanics have been built. The nature of these quantum computers is different to classical computers, and so programs for solving problems are designed very differently. Whilst a few tools have been developed to verify if quantum programs meet their desired behaviour, these are often hard to use for non-experts.

In this talk, I will describe Silq, a high-level programming language for quantum computing, and demonstrate SilVer, a tool I developed to verify Silq. I will discuss the design of SilVer and the use of automated provers (SMT solvers) for program verification.