Welcome to the SpecLeuven home page. SpecLeuven is a verifier for multithreaded programs written in the C# programming language. It is a research prototype, intended and licensed for non-commercial research and educational use only. See the License Agreement for details.

SpecLeuven is developed at the Department of Computer Science, Katholieke Universiteit Leuven, Belgium, by the SpecLeuven team, consisting of

• Bart Jacobs
• Frank Piessens
• Jan Smans

SpecLeuven is an extension and modification of the Spec# program verifier. Spec# is developed at Microsoft Research, Redmond, WA, USA, by the Spec# team, consisting of

• Mike Barnett
• Rob DeLine
• Rustan Leino
• Wolfram Schulte
• Herman Venter

with contributions by

• Bor-Yuh Evan Chang, UC Berkeley
• Manuel Fähndrich
• Bart Jacobs, K.U.Leuven
• Francesco Logozzo, École Normale Supérieure
• Peter Müller, ETH Zurich
• Madan Musuvathi
• Dave Naumann, Stevens Institute of Technology
• Simon Ou, Princeton
• Frank Piessens, K.U.Leuven
• River Sun, Stevens Institute of Technology

The SpecLeuven team uses the Spec# source code and releases binaries derived from the Spec# source code with Microsoft's permission.

Downloads

By downloading a SpecLeuven release, you agree to be bound by the SpecLeuven License Agreement.

• specleuven-3.0.zip (1.6 MB)
• specleuven-2.0.zip (1.6 MB)
• specleuven-1.0.zip (1.6 MB)

SpecLeuven 3.0 Release Notes

SpecLeuven 3.0 was tested with the following software installed:

• Windows XP Home Edition with Service Pack 2
• .NET Framework 2.0 (available through Windows Update)

You additionally need to install the Simplify theorem prover, as follows:

1. Download the Escjava release (not the Simplify release!) from the Java Programming Toolkit Source Release page on the HP Labs Downloads web site and save it to a file.
2. If the file name ends in .tar.tar, change it to .tar.Z.
3. Using a tool such as WinZip, extract the Escjava.tar.Z archive to a location on your computer.
4. Locate the file Simplify-1.5.4.exe.win in the folder Escjava/release/master/bin of the extracted archive, and copy it to the bin directory of the SpecLeuven installation.
5. Rename the file to Simplify.exe.

Changes

Major changes with respect to the previous release:

• Added support for assembly-scoped visible-state-based invariants. This is especially useful for concurrent programs. See the new sample fork-join.
• Added support for assembly-scoped rely-guarantee conditions. See the new sample increasing-counter. Note: mentioning Thread.CurrentThread in rely-guarantee conditions is not yet supported.
• The lock levels of class type objects are now implicitly ordered in the reverse program order (i.e. the lock level of the class that appears first in the program text is above the lock level of the class that appears second, etc.)
• Added support for state_independent_invariant declarations. An object's state-independent invariants must be monotonic (i.e. preserved by execution steps), it must hold before the base class constructor is called, and it is assumed whenever a field of the object is read.
• [StrictReadonly, LockProtected] fields must point to a [LockProtected] object when the base class constructor is called; the analogous requirement holds for [StrictReadonly, Immutable] fields.
• Added support for [LockProtected] classes. A parameter whose type is a [LockProtected] class is [LockProtected] by default.
• Added support for static fields and class constructors. See the new sample account-transfer.
  • Static fields of class C are conceptually thought of as residing in the most derived frame of the typeof(C) object.
  • Accessing a static field of class C requires that typeof(C) is appropriately accessible.
  • Static class invariants, static rep fields, and static expose blocks are not yet supported.
  • For verification of visible-state-based invariants: class objects are known to be unshared initially.
  • typeof(C) is implicitly shared as lock-protected at the bottom of the static constructor of class C.
  • An assumption that typeof(C) is shared is inserted at the top of the static methods and the constructors of class C.
  • To prevent deadlocks involving class initialization, class C must be below the lockset on entry to a static method or constructor of C, and class C must be locked when accessing a field of C.

SpecLeuven 2.0 Release Notes

SpecLeuven 2.0 was tested with the following software installed:

• Windows XP Home Edition with Service Pack 2
• .NET Framework 2.0 (available through Windows Update)

You additionally need to install the Simplify theorem prover, as follows:

1. Download the Escjava release from the Java Programming Toolkit Source Release page on the HP Labs Downloads web site and save it to a file.
2. If the file name ends in .tar.tar, change it to .tar.Z.
3. Using a tool such as WinZip, extract the Escjava.tar.Z archive to a location on your computer.
4. Locate the file Simplify-1.5.4.exe.win in the folder Escjava/release/master/bin of the extracted archive, and copy it to the bin directory of the SpecLeuven installation.
5. Rename the file to Simplify.exe.

Changes

Major changes with respect to the previous release:

• Added a LinkedList sample that appends two doubly-linked lists in constant space and time, transfering ownership of the nodes of list 1 to list 2.
• Methods are now verified one assertion and one path to the assertion at a time.
• Added support for [NoInvariant] classes. Assigning to a field of a [NoInvariant] class does not require exposing the target object, but [NoInvariant] classes cannot declare object invariants or rep fields.
• Added the ProverMatchDepth attribute.
• A Spec# quantifier with at least one filter is now translated into a BoogiePL quantifier with two triggers: one containing all filters, and one containing the body. This is useful to avoid matching loops in Simplify.

SpecLeuven 1.0 Release Notes

SpecLeuven 1.0 was tested with the following software installed:

• Windows XP Home Edition with Service Pack 2
• .NET Framework 2.0 (available through Windows Update)

You additionally need to install the Simplify theorem prover, as follows:

1. Download the Escjava release from the Java Programming Toolkit Source Release page on the HP Labs Downloads web site and save it to a file.
2. If the file name ends in .tar.tar, change it to .tar.Z.
3. Using a tool such as WinZip, extract the Escjava.tar.Z archive to a location on your computer.
4. Locate the file Simplify-1.5.4.exe.win in the folder Escjava/release/master/bin of the extracted archive, and copy it to the bin directory of the SpecLeuven installation.
5. Rename the file to Simplify.exe.

Changes

SpecLeuven 1.0 is based on the April 2006 Spec# release, except for the program verifier component (Boogie), which is based on the November 2005 release.

Major changes:

• Added support for C#'s lock statements
• The parser now accepts method contracts on delegate types
• Boogie now checks conformance of a delegate's target method with the delegate's contract
• Added support for [Captured] parameters
• Extended BoogiePL with support for typed struct fields and nested lvalues
• Heap encoding changed
• Support added for state abstraction using [Confined] methods
• Added support for [Confined] static methods; these are considered confined in their first argument
• Added support for immutable objects
• Method frame conditions are now derived from the writability conditions in the method's precondition instead of its modifies clause. Modifies clauses are ignored now.
• Added deadlock prevention support
• Added loop framing. A loop's frame condition is derived from its loop invariant.

This page authored by: the SpecLeuven team