Calvin

Calvin is a tool for checking safety properties of multithreaded Java programs. To handle realistic programs, Calvin performs modular checking of each procedure called by a thread using specifications of other procedures and other threads. The checker leverages off existing sequential program verification techniques based on automatic theorem proving. The Java programs we have applied Calvin to include the Apprentice challenge problem, the Mercator web crawler, and some Java libraries.

Here's the most up-to-date journal paper describing Calvin.

Modular Verification of Multithreaded Programs.

Cormac Flanagan, Stephen N. Freund, Shaz Qadeer and Sanjit A. Seshia.

Theoretical Computer Science, Volume 338, Issues 1-3, 10 June 2005, pp. 153-183.

An earlier version was published at CAV'02. (This is superseded by the paper above.)

A Modular Checker for Multithreaded Programs.

Cormac Flanagan, Shaz Qadeer and Sanjit A. Seshia.

In Proc. Computer-Aided Verification (CAV), LNCS 2404, Copenhagen, Denmark, July 2002.

The Calvin project was started by Shaz Qadeer, Stephen Freund, and Cormac Flanagan while they were at Compaq Systems Research Center. Since then, they have pursued other very interesting research directions in the area of verifying multithreaded software.

Calvin's code, which is based on ESC/Java, used to be publicly available from Compaq/HP Research, but it looks like it's no longer online.