Master's Thesis

Summary

Supporting multiple proof engines by translating between intermediate verification languages
Master's Thesis, March 2015 — September 2015
Author: Michael Ameri
Supervisor: Carlo A. Furia
Project plan
Project report

Description

Program verifiers are normally built on top of back-end proof engines. In such setups, the verifier encodes the semantics of the high-level input language (instructions, memory model, specification, and annotations for verification) into an intermediate language, which is then used to efficiently generate verification conditions for different proof engines. The two most widely used intermediate verification languages are Boogie and Why. The goal of this project is designing and implementing a translation of Boogie programs into Why programs. The translation will make it possible to use the Why system as a back-end for verifiers that output Boogie code.