Viper: A Verification Infrastructure for Permission-Based Reasoning

Static program verification has advanced significantly through the use of intermediate languages like Boogie and Why, which simplify the development of verifiers by providing a common target for front-end tools. However, these existing infrastructures are built on first-order logic and lack native support for permission-based logics, such as separation logic, which are essential for reasoning about heap-manipulating and concurrent programs. Consequently, developers of permission-based verifiers have historically been forced to build custom reasoning engines for each new tool.

Viper addresses this gap by providing an intermediate language that natively supports an expressive permission model. This infrastructure allows front-end developers to encode high-level language features and verification techniques while offloading the complex task of verification to Viper's back-end tools. Viper currently includes two primary back-end verifiers: one based on symbolic execution and another based on verification condition (VC) generation. By providing a reusable, automated back-end, Viper enables researchers and tool developers to focus on higher-level reasoning abstractions rather than the underlying theorem proving mechanics.

Viper's intermediate language is designed to be both human-readable and highly expressive. It supports several advanced features for managing heap structures, including:

• Recursive Predicates: Used to define and abstract over complex, recursive heap data structures.
• Magic Wands: A connective that allows for the representation of partial heap states, facilitating reasoning about data structures with missing components.
• Quantified Permissions: Allows for pointwise specification of heap locations, which is particularly useful for arrays and other non-hierarchical data structures.
• Custom Domains: Enables the definition of first-order mathematical theories, allowing users to introduce custom types and axioms to model specific domain knowledge.

Viper significantly reduces the barrier to entry for building automated verifiers. By standardizing the intermediate representation for permission-based reasoning, it allows for the rapid prototyping of new verification techniques and facilitates the comparison of different back-end strategies. As demonstrated by its adoption in projects like VerCors, Viper provides a more streamlined and efficient alternative to previous tool chains, enabling more complex programs to be verified with greater ease and performance.