Summer School in Software Engineering and Verification

Preparing for the school


Suggested reading

Compilers: Principles, Techniques, and Tools (the Dragon book) by Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman

Hardware

Please bring a laptop that is capable of running the software below.

Software

Please download the following software and have it on your laptop before the School:

VCC

VCC: A recent VCC build, which can be downloaded from http://vcc.codeplex.com, and a version of Visual Studio 2010 that supports C/C++. The easiest option is probably the express version A full Vistual Studio version (obtained, for example, through an academic license of their university), would work even better.

SatAbs

In this assignment you will practice with the SatAbs verification system and indirectly with the SMV tool, used by SatAbs as a model checker. Cadence SMV can be dowloaded from Ken McMillan's website http://www.kenmcmil.com/.

First you will need to fill a form, then you will be given installation instructions and links to binaries. Depending on your machine, to avoid compatibility issues, please download all the three available SMV versions.

SatAbs can be downloaded from http://www.cprover.org/satabs/, together with a detailed manual; please follow the installation instructions of Section 2.2 .

SatAbs, which uses a counterexample-guided abstraction refinement strategy, is a tool for verifying properties about C programs: it checks buffer overflows, pointers safety, division by zero and properties specified by users in form of assertions. An easy introduction to SatAbs can be found in Chapter 4 of the manual.