CheckFence Homepage

Welcome to CheckFence!


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.

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 ( by following the 'Mailing Lists' tab.


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.


Our code is being released under a BSD-style license. Logo