These pages contain a collection of textbook
examples that have been verified using the Spec#
programming language, the Spec# compiler and
the Spec# static program verifier.

A tutorial on Program Verification using the Spec# Programming System, presented at ECOOP 2009 is available here.

Our paper on the automatic verification of textbook
programs that use comprehensions is available here.
This work was presented at Formal Techniques for Java-
like Programs, ECOOP Workshop (FTfJP'07: July 2007,
Berlin, Germany).

Slides used in this presentation are available here.