Viper is a framework for automatic software verification. It supports a range of source code languages, where programs can be annotated with a formal specification. Viper then automatically attempts to prove that the program indeed complies with this specification. While impressive in small examples, Viper shows its limitations in many complex real-world programs (often those most in need of verification). Here Viper can feel not so automatic, and not so able to verify. These limitations are shared by all major automatic verifiers, which are built on SMT solvers. To overcome this, we investigate ways to integrate interactive proof methods within Viper's automatic processes - retaining automation when it works, but allowing easier interaction when required.

This talk is an introduction to the Viper tool and its core capabilities. I highlight Viper's strengths compared to other automatic verifiers and demonstrate cases where automatic verification is efficient and effective. I then show cases where verification is less effective, motivating the need for more sophisticated interaction with the verifier.