Viper is a verification infrastructure that facilitates the development of program verifiers based on separation logic. It consists of the Viper intermediate verification language and two SMT-based verification back-ends that automate proof search and can be reused across different front-ends. These front-end express verification problems in Viper by encoding an input program, its specification, and often dedicated proof rules. These encodings are facilitated by Viper’s expressive separation logic, offering fractional permissions, inductive predicates, iterated separating conjunction, and magic wands.

This interactive tutorial explains how to use Viper and how to automate different verification problems by encoding them into the Viper language, for instance, to efficiently prototype new verification logics, or develop entire program verifiers.