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
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
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
used to be publicly available from Compaq/HP Research,
but it looks like it's no longer online.