Viper Roots

Analogous to the architecture of compilers, many verification tools are implemented as a sequence of translation steps from programs and specifications to proof obligations in a suitable logic. Proof obligations in such translational verifiers are often expressed via intermediate verification languages (IVL). The IVL of a translational verifier decouples the front-end (which encodes the semantics of the input program) from the back-end (which automates the proof search). Thus, back-ends can be re-used across many verifiers, which drastically reduces the effort of building verifiers and facilitates the use of a portfolio of reasoning approaches. Examples of translational verifiers include Prusti (for Rust), Nagini (for Python), Gobra (for Go), and external page VerCors (for Java) based on the Viper IVL, external page Corral and external page Dafny based on the external page Boogie IVL, as well as external page Frama-C (for C) and external page Krakatoa (for Java) based on the external page Why3 IVL.

Our goal is to increase the reliability of translational verifiers. To guarantee correctness of a translational verifier, one must guarantee correctness of its underlying logic justifying the translations, as well as the implementation of the verifier itself, which often consists of multiple thousands of lines of code. To address these points, we aim to find solutions to the following challenges: (1) The development of a meta-theoretical framework for soundness proofs justifying the verifier translations, and (2) the automatic generation of foundational proofs that reduce the trusted code base of translational verifier implementations.

To enable solutions for both of these challenges, a formal semantics for the IVL used in the translational verifier is required. The development of such a semantics is non-trivial for the Viper IVL, which can directly express resources via permissions in the style of separation logic. For instance, Viper supports the manipulation and inspection of permissions, which can lead to subtle errors in program verifiers when applying standard techniques such as method inlining without additional checks. As part of our efforts, we aim to give a formal semantics for Viper and to solve the challenges outlined above for translational verifiers based on Viper. We formalize our results in the Isabelle/HOL theorem prover.

Project Members

Thibault Dardinier
Peter Müller
Gaurav Parthasarathy
Michael Sammler
external page Alex Summers (UBC)