Master Thesis

Summary

Designing and implementing an intermediate verification language
Master Thesis at ITMO, State University in Saint Petersburg - Rusia - November 2011 - November 2012
Author: Anton Bannykh
Supervisor: Martin Nordio and Julian Tschannen

Description

An intermediate verification language (IVL) is an abstraction layer between programming language and a reasoning engine. Notable examples are Boogie and Why. There is a number of papers about automatic verification via translating code into Boogie of Why. Nevertheless those solutions are usually complex, not very flexible and require high level of expertise. Although there are examples of successful usage of those platforms, it is still at the research level. The main idea is to create in IVL with rich specification facilities.