USING BOOGIE 2 IN THE VERIFICATION OF SPEC# PROGRAMS
K. Rustan M. Leino - Microsoft Research
Rosemary Monahan - National University of Ireland
Download the Slides!
Download the Source Code!
In this workshop we present the Spec# Programming System, the verifier for Spec# programs.
Throughout our presentation we illustrate how the Spec# Programming System
can be used to verify programs in an object-oriented environment. The effect
will be two-fold: participants will be given the practical experience of using
the Spec# Programming System and they will learn about Boogie 2, the intermediate
representation language that Spec# programs are translated to before verification.
Through this knowledge participants will develop an understanding of how logical verification
conditions are generated in program verification tools.
In recent work we have encoded some verification benchmark programs in the
languages Dafny (a language that explores the dynamic frames style of specifications)
and Spec#. Both of these languages use Boogie 2 as their intermediate representation language.
We use these benchmark programs to demonstrate the contributions of Boogie 2 to program verification.
The intended audience includes any researchers or lecturers who are interested in program verification.
In particular, it will appeal to educators who are considering using Spec# for teaching and to programmers who wish
to learn about the Spec# verification methodology. Participants should havean understanding
of object oriented programming languages such as C#, C++ or Java and a basic
understanding of method preconditions and post-conditions.
Participants will be expected to bring their own laptops for use during the
TOPICS COVERED DURING THE WORKSHOP:
The Spec# Programming System consists of the Spec# programming language
which is an extension of C#, the Spec# compiler which is integrated into the
Microsoft Visual Studio development environment and the Spec# static program verifier which
translates Spec# programs into logical verification conditions. The result is an
automatic verification environment which establishes the correctness of a program before allowing
it to be executed. In addition to the run-time checking traditionally found in the
design by contract approach, Spec# offers the possibility to verify contracts
statically. The goal of this analysis is to help programmers to detect errors more quickly than they
might be found by traditional methods, hence providing an opportunity to correct the
errors when they are still relatively cheap to fix. A unique feature of the Spec#
Programming System is its guarantee of maintaining invariants in object-oriented programs in
the presence of callbacks, threads and inter-object relationships. In addition, the Spec#
Programming System has been extended so that programs that involve the mathematical
domains that are so familiar to textbook examples (such as sum, count, product, min, and
max) may be verified.
Boogie 2 is an intermediate verification language, intended as a layer on
which to build program verifiers for other languages. Several program verifiers have
been built in this way, including one for the object-oriented .NET language Spec#, the
HAVOC and vcc verifiers for C, the Dafny language and verifier, and the concurrent
language Chalice. Experience with some automatic program verifiers suggests that the
complex task of generating verification conditions for modern programming languages
can be managed by separating the task into two steps: a transformation of the
program and its proof obligations into an intermediate language, and then a
transformation of that intermediate-language program into logical formulae. If the verification
conditions can be proved correct (with the help of an automated theorem prover) the program
is verified as correct. If the verification conditions cannot be proved correct, it is
possible that errors occur in the program.
The presentation involving both of these languages will provide a detailed
description of one of the most successful systems for the static and dynamic analysis of
object-oriented programs. More precisely, topics discussed at the event will be as follows:
PART 1: THE SPEC# PROGRAMMING SYSTEM:
An overview of Spec#: Explaining what is Spec# and what is its tool suite.
Programming in the small: Worked examples that show the use of
preconditions, postconditions, loop invariants, and assert and assume statements.
Programming in the large: We introduce multi-method and multi-class
examples. We explain object invariants and how they can be maintained in the presence
of callbacks, threads, and inter-object relationships. We start with simple
single-object invariants and then go into ownership-based invariants and visibility-based
PART 2: BOOGIE 2 AS AN INTERMEDIATE REPRESENTATION LANGUAGE
An overview of Boogie 2:We give an overview of Boogie 2 using worked
examples to show its language constructs, types, expressions and statements.
Generating Boogie 2 programs from Spec# programs: We show the Boogie 2
programs that are generated by translating Spec# programs to its intermediate
In particular, we discuss important decisions (such as how to model
memory) that must be considered when translating a source language like
Spec# into Boogie 2.
Verifying benchmark programs in Spec# and Dafny: We use these benchmark
programs to compare the languages the features of these languages and their
capability for program verification.