Continuing Exercise 01

This course has a theoretical homework and a practical project part.

• Theoretical homework is to be solved individually and submitted through Moodle, so please register for the course, if you haven't been registered automatically. The enrollment key is: whatAFunCourse.
• Projects can be done individually or in groups of two, as you wish. We have an awesome version control and submission system based on Git, where you should register as well. The instructions for how to do this are on the bottom of this page.

General announcement will be also made through Moodle, so please register!

Before we start building our own verification system, let's try to use an existing one to prove some program properties. In particular, we will use the web-interface of Spec# (http://rise4fun.com/SpecSharp), which is a formal language built on top of C#, that can prove programs correct with respect to code contracts.

Code contracts

Fun with Spec#

The project consists of building a predicate abstraction engine. You will learn in detail what predicate abstraction is and how it works during the course. In rough terms, a predicate abstraction engine uses a set of predicates to abstract a program, i.e. to describe it in terms of a finite set of predicates. This abstraction will in general be an over-approximation of the program behavior, but it can be used to reason about certain program properties.

To get an idea of the final goal, you can download a jar file with a complete version of such an engine as well as some examples.

For your project, you will be given a skeleton and will implement the rest in approximately the following stages:

• creating a control-flow graph from a program
• merging of loop-free code fragments
• abstracting the program with a user-given set of predicates
• using interpolation from Princess to come up with a set of predicates automatically

As you can see from the description, the engine uses internally the Princess theorem prover and your first project task will be to become familiar with it and Presburger arithmetic (see Homework 01).