USING BOOGIE 2 IN THE VERIFICATION OF SPEC# PROGRAMS

K. Rustan M. Leino - Microsoft Research
Rosemary Monahan - National University of Ireland

8, November

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 Event.

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 invariants.

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 representation.
  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.