FM 2006

 
August 21 - 27, 2006
McMaster University
Hamilton ON, Canada

Submission Dates

Technical Papers, Workshops and Tutorials

Friday February 24, 2006

Posters and Tools, Doctoral Symposium

Friday May 26, 2006

 

Notification Dates

Technical Papers

Friday April 28, 2006

Workshops and Tutorials

Friday March 10, 2006

Doctoral Symposium

Wednesday June 14, 2006

Posters and Research Tools

Monday June 12, 2006


Contact Information

General Inquiries

General Chair

Emil Sekerinski

Program Chairs

Jayadev Misra,
Tobias Nipkow

Workshops Chair

Tom Maibaum

Tutorials Chair

Jin Song Dong

Tools & Poster Chair

Marsha Chechik

Industry Day Chairs

Volkmar Lotz,
Asuman Suenbuel

Doctoral Symposium Chair

Ana Cavalcanti

Augusto Sampaio

Jim Woodcock

Sponsorship Chair

Jürgen Dingel

T10 Spec#
Tutor:
Wolfram Schulte
Affiliation:
Microsoft Research, USA
Date:
August 26, 2006
Time:
9:00-12:30, 2:00-5:30, 1/2hr break at 10:30 and 3:30
Location:
ITB 238
Format:
Full-day. 4-45 minute lectures, and some interactive exercises with the Spec# system. Participants are welcomed to download Spec# and install it on their laptops. Lab computers will also be loaded with Spec#.
Slides available ( 1 2 3 4 5 )
 

Topic:

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software.  Spec# is pronounced "Spec sharp" and can be written (and searched for) as the "specsharp" or "Spec# programming system".  The Spec# system consists of:

  • The Spec# programming language.  Spec# is an extension of the object-oriented language C#.  It extends the type system to include non-null types and checked exceptions.  It provides method contracts in the form of pre- and postconditions as well as object invariants.
  • The Spec# compiler.  Integrated into the Microsoft Visual Studio development environment for the .NET platform, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools.
  • The Spec# static program verifier.  This component (codenamed Boogie) generates logical verification conditions from a Spec# program.  Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it.

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.

The Spec# programming system is being developed as a research project at Microsoft Research in Redmond, primarily by the Programming Languages and Methods group.

 

Objective:

 

Understand how a verifying compiler is build and what a verifying compiler can do.

 

Prerequisites:

 

Basic understanding of object-oriented programming, type system and Hoare Calculus or similar.

 

Biography of Tutor:

 

Since 2006 Wolfram Schulte has been a research area manager for the Foundations of Software Engineering (FSE) group, the Programming Language and Methods (PLM) group, and the Software Design and Improvment (SDI) group at Microsoft Research in Redmond, Washington, USA. The research of these groups tries to improve software development productivity through rigorous software design, design verification, new programming language features in conjunction with program verification, advanced test generation, and new programming language implementations for sequential, parallel and embedded hardware. In principle, Wolfram's research concerns the practical application of formal techniques. He has published a variety of papers in the areas of language design, verification, testing, program derivation and compilation. Before joining Microsoft Research in 1999, Wolfram worked at the University of Ulm (1993-1999), at sd&m, a German software company (1992-1993), and at the Technical University Berlin (1987-1992). http://research.microsoft.com/~schulte/