A Formal Semantics for the Viper Intermediate Language

Background

The Viper project, developed in our research group, provides a number of verification and inference tools based around a new intermediate verification language, suitable for encoding verification problems from higher-level concurrent programming languages. Automatic verifiers handle general problems encoded into Viper, ultimately via interaction with lower-level tools; developers of new verification tools can thus focus on implementing a translation of their source programming language and desired properties into Viper. For example, Viper is used as a platform for building tools which verify concurrent Java code and GPU programs.

When implementing a new verification tool via such a translation, it is natural to consider the soundness of the proposed encoding. This requires a formal semantics for the target language, but Viper is not executable - rather than an operational semantics, one requires a formal definition that expresses what it means to verify Viper programs. This has been achieved for small subsets of the language with a Hoare Logic formalisation and, indirectly, via a translation to weakest-preconditions. However, no formal semantics exists for the complete language, and many novel language features have no such definitions.

Project Aims

The goal of this project is to develop the first formal semantics for the Viper language as a whole. The precise formalism, as well as whether this is a mechanised or by-hand effort should be evaluated and decided upon during the project. The formalism should be connected to existing work on the underlying logic, and must also take into account the important factor that the semantics must be easy for clients of Viper to make use of for their own soundness proofs.

In order to exercise this new semantics, the project can be extended to prove soundness of the translation of (a subset of) Chalice, a research language for which an encoding into Viper is already implemented. This will provide evidence that the formal semantics is fit for purpose, as well as being an interesting result in its own right.

Useful Prerequisites

The following skills would be advantageous, but can also be learned during the project:

  • Background in Formal Methods, including program semantics.
  • Experience in constructing mathematical formalisms and proofs.
  • (Possibly) familiarity with proof assistants such as Coq or Isabelle.

Objectives and Outcomes

  • Familiarisation with the Viper intermediate language, including the language design and theoretical underpinnings.
  • Identification of a suitable formalism to tackle, including deciding on the use of tools (if any).
  • Development of a formal axiomatic semantics, with connection to existing work on, e.g. the assertion logic.
  • Understanding the Chalice translation, as an example of a front-end encoding into Viper.
  • Proof of the soundness of this translation, using the newly-developed formal semantics.

Contact

JavaScript has been disabled in your browser