CheckFence Homepage
Welcome
to CheckFence!
Introduction
CheckFence is a SAT-based
formal verification tool that analyzes C code
implementing concurrent data types on multiprocessors (concurrent
queues, sets etc.) with respect to a selected memory model.
- CheckFence soundly
verifies or falsifies the implementation for individual tests supplied
by the user, covering all possible instruction interleavings and
reorderings.
- CheckFence does not
require formal specifications or annotations, but mines a specification
directly from the C code (either from the implementation under test, or
from a reference implementation).
- CheckFence currently
supports a limited but reasonable subset of C, as required for typical
implementations. This subset includes conditionals, loops, pointers,
arrays, structures, function calls, locks, and dynamic memory
allocation.
- CheckFence lets the user
specify the desired memory model in an axiomatic format.
- If a test fails, CheckFence provides
an HTML-formatted counterexample trace that displays various views of
the execution and can be navigated using hyperlinks.
Project Updates
To keep informed about the current project status, visit our SourceForge
repository. If you would like to receive e-mail about release
status and documentation or website updates, you can subscribe to our
mailing list (checkfence-announce@sourceforge.net) by following the
'Mailing Lists' tab.
Downloads
As this project is just ramping up, we provide raw CVS releases only.
You can download the current code
(which should compile under most linux versions) and some very basic
installation instructions directly from the SourceForge
repository. We are still working on some documentation (including a
tutorial).
To run the front end, you will also need OCaml installed on
your system and the CIL package.
Project Members
The CheckFence project started as part of the PhD research of Sebastian Burckhardt,
under the guidance of his advisors Prof. Rajeev Alur and Prof. Milo Martin.
License
Our code is being released under a BSD-style license.
