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.


Throughout the tutorial 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.

More precisely, topics discussed at the event will be as follows:

    * 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.
    * An overview of Boogie 2: We give an overview of Boogie 2 to show its language constructs, types, expressions and statements.
    * Generating Boogie 2 programs from Spec# programs: We show examples of Boogie 2 programs that are generated by translating Spec# programs to its intermediate representation.


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 have an 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. There is no need to install any software in advance of the tutorial. Presenter Information:

Rosemary Monahan is a Lecturer at the National University of Ireland, Maynooth (NUIM), where she lectures on topics such as program verification, program language semantics and computer programming. Rosemary’s research, as part of the Principles of Programming (PoP) research group, is concerned with the static and dynamic analysis of object-oriented programs.