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. Slides and examples from workshops and tutorials follow:

SBMF 2010: Using Boogie 2 in the verification of Spec# programs.

IFM 2010: Verification of C# programs using Spec# and Boogie 2 .

Specsharp and Boogie code examples from IFM 2010 and SBMF 2010 are available for download from here.

ECOOP 2009: Program Verification using the Spec# Programming System.

Papers on the Automatic Verification of textbook programs that use Comprehensions and about Reasoning about Comprehensions with First-Order SMT Solvers
were published at FTfJP'07 and SAC 2008.

Slides used in the FTfJP'07 presentation are available here.