A formal semantics for Viper
Abstract
The Verification Infrastructure for Permission-based Reasoning (Viper) is a suite of tools developed by the Chair of Programming Methodology research group at ETH Zurich. Viper includes an intermediate language which is based on a flexible permission model and aims to allow for simple encodings of permission-based reasoning techniques implemented in front-end tools such as Chalice. As of today, the intermediate language of Viper lacks a formal semantics. Thus, encodings of front-end languages into Viper cannot formally be reasoned about and the verification of a program encoded into Viper cannot rigorously be argued to be sound with respect to the semantics of the front-end tool language. This thesis presents the first formal semantics for a chosen subset of Viper. Moreover, an encoding [_] of a subset of Chalice into Viper is defined and proven sound: if an encoded Chalice program [p] verifies with respect to the semantics of Viper then p verifies with respect to the semantics of Chalice.